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.
https://hal.archives-ouvertes.fr/hal-02420590
Contributor : Sylvain Conchon <>
Submitted on : Friday, December 20, 2019 - 8:45:34 AM Last modification on : Tuesday, December 8, 2020 - 10:08:54 AM Long-term archiving on: : Saturday, March 21, 2020 - 1:36:52 PM
Sylvain Conchon, David Declerck, Fatiha Zaïdi. Cubicle-W: Parameterized Model Checking on Weak Memory. IJCAR 2018 - International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.152-160. ⟨hal-02420590⟩