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: 1 Publication 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 Cited by 3 Authors 1 Di Giusto, Cinzia 1 Guizouarn, Loïc Germerie 1 Lozes, Etienne Cited in 1 Serial 1 Journal of Logical and Algebraic Methods in Programming Cited in 1 Field 1 Computer science (68-XX) Citations by Year