Abstract
Cubicle is a new model checker for verifying safety properties of parameterized systems. It implements a parallel symbolic backward reachability procedure using Satisfiabilty Modulo Theories. Experiments done on classic and challenging mutual exclusion algorithms and cache coherence protocols show that Cubicle is effective and competitive with state-of-the-art model checkers. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Conchon, S., Goel, A., Krstić, S., Mebsout, A., & Zaïdi, F. (2012). Cubicle: A parallel SMT-based model checker for parameterized systems: Tool paper. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7358 LNCS, pp. 718–724). https://doi.org/10.1007/978-3-642-31424-7_55
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
