Programming Languages Delft<p>Master thesis by Michał Raczkiewicz: "Model Checking Under JAM21"</p><p>"This thesis presents the first known implementation of a model checker for the Java memory model JAM21 within the GenMC framework - a tool for stateless model checking using custom memory models. [..] We provide a formal proof of equivalence between the new vector clock algorithm and the original implementation to ensure correctness."</p><p><a href="https://repository.tudelft.nl/record/uuid:3c4c7d73-b084-4a4d-9d6d-93256bc09598" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/record/u</span><span class="invisible">uid:3c4c7d73-b084-4a4d-9d6d-93256bc09598</span></a></p><p><a href="https://akademienl.social/tags/Java" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Java</span></a> <a href="https://akademienl.social/tags/ModelChecking" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>ModelChecking</span></a> <a href="https://akademienl.social/tags/MemoryModels" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>MemoryModels</span></a> <a href="https://akademienl.social/tags/FormalProofs" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>FormalProofs</span></a> <a href="https://akademienl.social/tags/master" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>master</span></a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>thesis</span></a></p>