| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [22 references]
https://hal.archives-ouvertes.fr/hal-02420590
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
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
File
paper.pdf
Files produced by the author(s)