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.
CITATION STYLE
Conchon, S., Declerck, D., & Zaïdi, F. (2018). Cubicle-W: Parameterized Model Checking on Weak Memory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 152–160). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_11
Mendeley helps you to discover research relevant for your work.