101010.pl

Programming Languages DelftMaster thesis by Pepijn Vunderink: "Program Matching with Semantic Patterns""We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs."<a href="https://repository.tudelft.nl/record/uuid:a18ab135-96b1-417c-b25e-46aa02521896" rel="nofollow noopener" translate="no" target="_blank">https://repository.tudelft.nl/record/uuid:a18ab135-96b1-417c-b25e-46aa02521896</a><a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener" target="_blank">#thesis</a> <a href="https://akademienl.social/tags/PatternMatching" class="mention hashtag" rel="nofollow noopener" target="_blank">#PatternMatching</a> <a href="https://akademienl.social/tags/MuCalculus" class="mention hashtag" rel="nofollow noopener" target="_blank">#MuCalculus</a> <a href="https://akademienl.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#ModelChecking</a> <a href="https://akademienl.social/tags/mCRL2" class="mention hashtag" rel="nofollow noopener" target="_blank">#mCRL2</a>

Rob SisonThere'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:<a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener" translate="no" target="_blank">https://youtu.be/7wcFx6OTEL4</a><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener" target="_blank">#sel4summit</a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#seL4</a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#verification</a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener" target="_blank">#operatingsystems</a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener" target="_blank">#microkernel</a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#HOL4</a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#modelchecking</a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalmethods</a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formalverification</a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener" target="_blank">#formal_methods</a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener" target="_blank">#formal_verification</a>

Programming Languages DelftMaster thesis by Matteo Meluzzi: Model Checking the XMM Memory Model"we present our design of a model checker algorithm for the XMM memory model called GenMC-XMM [...] GenMC-XMM is the first multi-execution model checker proven to be sound. We evaluated our tool against the state-of-the-art model checking tools for RC11, IMM, and Weakestmo2."<a href="https://repository.tudelft.nl/record/uuid:93937121-ae62-4253-a716-d3c911d85e9c" rel="nofollow noopener" translate="no" target="_blank">https://repository.tudelft.nl/record/uuid:93937121-ae62-4253-a716-d3c911d85e9c</a><a href="https://akademienl.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#ModelChecking</a> <a href="https://akademienl.social/tags/compilers" class="mention hashtag" rel="nofollow noopener" target="_blank">#compilers</a> <a href="https://akademienl.social/tags/multiexecution" class="mention hashtag" rel="nofollow noopener" target="_blank">#multiexecution</a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener" target="_blank">#thesis</a>

Ivan Enderlin 🦀A Practical Approach for Model Checking C/C++11 code, <a href="http://plrg.eecs.uci.edu/publications/toplas16.pdf" rel="nofollow noopener" translate="no" target="_blank">http://plrg.eecs.uci.edu/publications/toplas16.pdf</a>.<a href="https://fosstodon.org/tags/testing" class="mention hashtag" rel="nofollow noopener" target="_blank">#testing</a> <a href="https://fosstodon.org/tags/safety" class="mention hashtag" rel="nofollow noopener" target="_blank">#safety</a> <a href="https://fosstodon.org/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#ModelChecking</a> <a href="https://fosstodon.org/tags/cpp" class="mention hashtag" rel="nofollow noopener" target="_blank">#cpp</a>

Dirk-Jan SwagermanMostly, software interfaces are only defined by their signature and without a formal description of the admissible behavior and timing assumptions.<a href="https://systems.social/tags/ComMA" class="mention hashtag" rel="nofollow noopener" target="_blank">#ComMA</a> provides a family of domain-specific languages that integrate existing techniques from formal behavioral and time modeling and is easily extensible.<a href="https://youtu.be/-bbJTg7pJ-k" rel="nofollow noopener" target="_blank">https://youtu.be/-bbJTg7pJ-k</a><a href="https://systems.social/tags/SoftwareEngineering" class="mention hashtag" rel="nofollow noopener" target="_blank">#SoftwareEngineering</a> <a href="https://systems.social/tags/Interfaces" class="mention hashtag" rel="nofollow noopener" target="_blank">#Interfaces</a> <a href="https://systems.social/tags/Modelling" class="mention hashtag" rel="nofollow noopener" target="_blank">#Modelling</a> <a href="https://systems.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#ModelChecking</a> <a href="https://systems.social/tags/CodeGeneration" class="mention hashtag" rel="nofollow noopener" target="_blank">#CodeGeneration</a>

Recent searches

Search options

Administered by:

Server stats:

#modelchecking