Cubicle: a parallel SMT-based model checker for parameterized systems: tool paper

CAV, pp. 718-724, 2012.

Cited by: 0|Bibtex|Views5|Links
EI
Keywords:
reachability proceduretool paperparameterized systemmutual exclusion algorithmcache coherence protocolMore(5+)

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...More

Code:

Data:

Your rating :
0

 

Tags
Comments