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 metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02420590
Contributor : Sylvain Conchon <>
Submitted on : Friday, December 20, 2019 - 8:45:34 AM
Last modification on : Tuesday, April 21, 2020 - 1:05:58 AM
Document(s) archivé(s) le : Saturday, March 21, 2020 - 1:36:52 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02420590, version 1

Citation

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⟩

Share

Metrics

Record views

38

Files downloads

18