Skip to Main content Skip to Navigation
Conference papers

Cubicle-W: Parameterized Model Checking on Weak Memory

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 metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Sylvain Conchon Connect in order to contact the contributor
Submitted on : Friday, December 20, 2019 - 8:45:34 AM
Last modification on : Friday, January 21, 2022 - 3:10:28 AM
Long-term archiving on: : Saturday, March 21, 2020 - 1:36:52 PM


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. IJCAR 2018 - International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.152-160. ⟨hal-02420590⟩



Les métriques sont temporairement indisponibles