Cubicle: a parallel smt-based model checker for parameterized systems. 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.
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Li, Yongjian; Pang, Jun; Lv, Yi; Fan, Dongrui; Cao, Shen; Duan, Kaiqiang: ParaVerifier: an automatic framework for proving parameterized cache coherence protocols (2015)
- Bertolissi, Clara; Ranise, Silvio: Verification of composed array-based systems with applications to security-aware workflows (2013)
- Conchon, Sylvain; Goel, Amit; Krstić, Sava; Mebsout, Alain; Zaïdi, Fatiha: Cubicle: a parallel SMT-based model checker for parameterized systems. Tool paper (2012)