Mcmt swMATH ID: 11911 Software Authors: Ghilardi S, Ranise S Description: Mcmt: a model checker modulo theories. We describe mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state systems whose state variables are arrays. Theories specify the properties of the indexes and the elements of the arrays. Sets of states and transitions of a system are described by quantified first-order formulae. The core of the system is a backward reachability procedure which symbolically computes pre-images of the set of unsafe states and checks for safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques, efficient heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart of the system. mcmt has been successfully applied to the verification of imperative programs, parametrised, timed, and distributed systems. Homepage: http://link.springer.com/chapter/10.1007/978-3-642-14203-1_3 Related Software: SAFARI; Cubicle; z3; SMT-LIB; MathSAT5; CVC4; Booster; ASASP; Yices; VERIFAS; OpenSMT; SIMPLIFY; nuXmv; SeaHorn; CPAchecker; Maude; veriT; Uppaal; FunArray; Princess Cited in: 23 Publications all top 5 Cited by 31 Authors 13 Ghilardi, Silvio 6 Ranise, Silvio 6 Sharygina, Natasha 5 Alberti, Francesco 5 Gianola, Alessandro 4 Calvanese, Diego 4 Montali, Marco 4 Rivkin, Andrey 2 Bruttomesso, Roberto 1 Barrett, Clark W. 1 Bertolissi, Clara 1 Bjørner, Nikolaj S. 1 Conchon, Sylvain 1 Declerck, David 1 Heidarian, Faranak 1 Hyvärinen, Antti E. J. 1 Itzhaky, Shachar 1 Kapur, Deepak 1 Karbyshev, Aleksandr 1 Lisitsa, Alexei P. 1 Marescotti, Matteo 1 Meseguer Guaita, José 1 Muñoz, César A. 1 Pagani, Elena 1 Rinetzky, Noam 1 Rocha, Camilo 1 Schmaltz, Julien 1 Shoham, Sharon 1 Tinelli, Cesare 1 Vaandrager, Frits W. 1 Zaïdi, Fatiha all top 5 Cited in 6 Serials 5 Journal of Automated Reasoning 2 Formal Methods in System Design 2 Logical Methods in Computer Science 2 Journal of Logical and Algebraic Methods in Programming 1 Theoretical Computer Science 1 MSCS. Mathematical Structures in Computer Science Cited in 2 Fields 23 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) Citations by Year