Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
veganism.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Veganism Social is a welcoming space on the internet for vegans to connect and engage with the broader decentralized social media community.

Administered by:

Server stats:

293
active users

veganism.social: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.0-alpha.5

#modelchecking

0 posts0 participants0 posts today
Jan :rust: :ferris:<p>ESBMC - An Efficient SMT-based Bounded Model Checker</p><p><a href="https://ssvlab.github.io/esbmc/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">ssvlab.github.io/esbmc/</span><span class="invisible"></span></a></p><p>"ESBMC is an open-source, [...], context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well."</p><p>1/3</p><p><a href="https://floss.social/tags/SMT" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SMT</span></a> <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a> <a href="https://floss.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a></p>
Andrew Helwer<p>Understandable &amp; predictable performance has its benefits!</p><p><a href="https://discuss.systems/tags/FormalMethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalMethods</span></a> <a href="https://discuss.systems/tags/TLAPlus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>TLAPlus</span></a> <a href="https://discuss.systems/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>formal_verification</span></a></p>
Dirk-Jan Swagerman<p>Mostly, software interfaces are only defined by their signature and without a formal description of the admissible behavior and timing assumptions.</p><p><a href="https://systems.social/tags/ComMA" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ComMA</span></a> provides a family of domain-specific languages that integrate existing techniques from formal behavioral and time modeling and is easily extensible.</p><p><a href="https://youtu.be/-bbJTg7pJ-k" rel="nofollow noopener" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/-bbJTg7pJ-k</span><span class="invisible"></span></a></p><p><a href="https://systems.social/tags/SoftwareEngineering" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>SoftwareEngineering</span></a><br><a href="https://systems.social/tags/Interfaces" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Interfaces</span></a><br><a href="https://systems.social/tags/Modelling" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Modelling</span></a><br><a href="https://systems.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a><br><a href="https://systems.social/tags/CodeGeneration" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>CodeGeneration</span></a></p>
VegansExploreLive feeds
About