Cubicle-W: Parameterized Model Checking on Weak Memory

Sylvain Conchon 1, 2 David Declerck 1, 2 Fatiha Zaïdi 3, 1
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
3 ForTesse
LRI - Laboratoire de Recherche en Informatique
Abstract : We present Cubicle-W, a new version of the Cubicle model checker to verify parameterized systems under weak memory models. Its main originality is to implement a backward reachability algorithm modulo weak memory reasoning using SMT. Our experiments show that Cubicle-W is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download
Contributor : Sylvain Conchon <>
Submitted on : Friday, December 20, 2019 - 8:45:34 AM
Last modification on : Thursday, January 23, 2020 - 1:31:03 AM


Files produced by the author(s)


  • HAL Id : hal-02420590, version 1


Sylvain Conchon, David Declerck, Fatiha Zaïdi. Cubicle-W: Parameterized Model Checking on Weak Memory. International Joint Conference on Automated Reasoning - IJCAR 2018, Jul 2018, Oxford, United Kingdom. pp.152-160. ⟨hal-02420590⟩



Record views


Files downloads