(S)SBMC  SMTbased Stochastic Bounded Model Checking
Subproject 
S3 
Categories 
Model checker / solver for probabilistic systems 
Overview 
(S)SBMC generates counterexamples for probabilistic systems, namely DiscreteTime Markov Chains (DTMCs) and Markov Reward Models (MRMs) with discretetime. This is done by computing a set of paths which fulfil a given property. The total probability of this set exceeds a given probability bound. The basic computation is done with Bounded Model Checking using the SATsolver MiniSat (in case of SBMC) or the SMTsolver Yices (in case of SSBMC). There exist several features:  Loop Detection speeds up the computation,  Bisimulation Minimization downsizes the system,  Path Conversion converts minimized paths back to the original ones. The SMTbased variant SSBMC is able to find paths with a higher probability first, thus generating smaller counterexamples than with SAT. SSBMC also allows to generate counterexamples for MRMs. In case of the latter, the search space might be restricted to a given reward interval, so that only paths with a reward within the interval are considered. 
B. Braitling, R. Wimmer, B. Becker, N. Jansen, and E. Ábrahám. Counterexample generation for Markov chains using SMTbased bounded model checking. In Roberto Bruni and Jürgen Dingel, editors, Proceedings of the 13th IFIP International Conference on Formal Methods for Open Objectbased Distributed Systems (FMOODS) / 31st IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), volume 6722 of Lecture Notes in Computer Science, pages 7589, 2011. R. Wimmer, B. Braitling, and B. Becker. Counterexample generation for discretetime Markov chains using bounded model checking. In Neil D. Jones and Markus MüllerOlm, editors, Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), number 5403 in Lecture Notes in Computer Science (LNCS), pages 366380, 2009 

Contract Signing Protocol, Crowds Protocol, Synchronous Leader Election Protocol, Selfstabilizing Minimal SpanningTree Algorithm 

Download 
Click here for the binary. 
Manual 
Just type ./sbmc (respectively ./ssbmc) to see how the tool can be used and to receive information about the available options. 
Status 
Prototype 