×

McScM

swMATH ID: 14482
Software Authors: Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire
Description: McScM: A general framework for the verification of communicating machines. We present McScM, a platform for implementing and comparing verification algorithms for the class of finite-state processes exchanging messages over reliable, unbounded FIFO channels. McScM provides tools for the safety verification and controller synthesis of these infinite-state models. Our verification tool implements several model-checking techniques: CEGAR with different abstraction-refinement methods, abstract interpretation, abstract regular model checking, and lazy abstraction. Seen as a general framework for the class of transition systems with finite control/infinite data, McScM delivers the basic infrastructure for implementing verification algorithms, and privileges to conveniently implement new ideas on a high level of abstraction. It also allows us to compare and benchmark different algorithmic approaches with the same backend.
Homepage: http://link.springer.com/chapter/10.1007%2F978-3-642-28756-5_34
Related Software: TaPAS; CADP; SPIN; TREX
Cited in: 2 Documents

Standard Articles

1 Publication describing the Software Year
McScM: a general framework for the verification of communicating machines
Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire
2012

Citations by Year