MCMT: Model Checker Modulo Theories

Download

MCMT is distributed "as is" without warranty of any kind; it is free for non-commercial use. It is possible to download the executables for Linux 64 bit and for Mac_OS systems together with some examples. The executables for the old versions can be required to the author. A version 3.0 linked to the SMT solver Z3 from Microsoft Research is available here.

Instructions

You can run MCMT via command line; for detailed explanations, please, have a look at the User Manual. MCMT must be linked to the SMT solvers Yices1 or Z3.

Experiments

We run MCMT on various examples: parametrized mutual exclusion and cache coherence protocols, timed systems, imperative programs, etc. These experiments show the great flexibility of the tool. All the files for these examples are included in the distribution (in each file, a brief description of the source and the meaning of the example is supplied). Table with experimental statistics (concerning the old version 1.0) are available here. Further case studies have been analyzed:

• Parameterized Timed Systems: some benchmarks in this area (Fischer mutual exclusion, csma, etc.) are available in the distribution;

• Mutual exclusion, deadlock freedom and waiting time bounds for Fischer and Lynch-Shavit algorithms: see the related paper here;

• Fault Tolerant Systems: reliable broadcast algorithms from Chandra-Toueg papers have been studied with MCMT; see here and here for more information;

• ARP Internet protocol: the protocol, as well as known attacks, has been analyzed with MCMT, see here for more information;

• Imperative programs: these benchmarks concern standard functions on strings and unbounded arrays (like copying, comparing, searching, etc.) where the abstraction and acceleration features of version 2.0 are exploited; benchmarks files are available in the distribution.

• Database driven systems: these benchmarks are supported in the new version 2.8 (see the User Manual and the benchmarks in the distribution).

Related Tools

Swarm Safety Detector SAFE is a web tool that employs verification techniques on parameterized multi-agent systems (PMASs), and, in particular, checks whether states satisfying a given goal formula, which existentially quantifies over the existence of agents, are reachable in a given MAS. SAFE automatically transforms PMASs into an array-based system representation, ready to be verified by MCMT. More information and download here.

The tools ArCa and ArCa_Sat analyze model-checking and satisfiability problems involving arrays and cardinality constraints; the tool ArCa_Sim produces counters simulations for such problems. Click here for more information and for for download.

The tool Booster is an integrated framework: it supplies a front-end to a C fragment and is able to run different copies of MCMT, trying in parallel the most promising settings. Booster is recommended for people interested in software model checking applications (contact T. Alberti for more information).

The tool ASASP analyzes security access policies within the model checking modulo theories framework. SAFARI (no longer maintained) is a re-implementation of MCMT, comprising abstraction/refinement capabilities. Cubicle implements the array-based MCMT framework in a parallel architecture.

Aknowledgements

The tool is currently developed and maintained by Silvio Ghilardi. Other people were involved in the history of the tool. Silvio Ranise was part of the MCMT project since the very beginning, co-founded it and contributed to it until he left for an FBK position. Thanks are due to R. Bruttomesso and F. Alberti for various help in the developement of past versions of the tool.

Some Publications

• Theoretical framework.
  S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Towards SMT Model-Checking of Array-based Systems In Proc. of IJCAR'08 (extended version).
  S. Ghilardi and S. Ranise, Backward Reachability of Array-based Systems by SMT Solving: Termination and Invariant Synthesis, Logical Methods in Computer Science, vol.6, n.4, 2010.

• Stopping failures / Approximated Models.
  F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G. Rossi Universal guards, relativization of quantifiers, and failure models in model checking modulo theories, Journal on Satisfiability, Boolean Modeling and Computation (JSAT), vol. 8, pp. 29-61, 2012.

• Abstraction and acceleration features.
  F. Alberti, R. Bruttomesso, S, Ghilardi, S. Ranise, N. Sharygina Lazy Abstraction with Interpolants for Arrays, Proceedings of LPAR-18, Springer LNCS, 2012;
  F. Alberti, S. Ghilardi, N. Sharygina Definability of Accelerated Relations in a Theory of Arrays and its Applications, Proc. of FroCoS 13, Springer LNCS, 2013;

• Database Applications.
  D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin SMT-based Verification of Data-Aware Processes: a Model-Theoretic Approach, Mathematical Structures in Computer Science, 2020 (arXiv very preliminary version available here).
  D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin From Model Completeness to Verification of Data Aware Processes, in "Description Logics, Theory Combinations, and All That", Springer Festschtift, LNCS 11560, pp.212-239, 2019.
  D. Calvanese, S. Ghilardi, A. Gianola, M. Montali, A. Rivkin Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN, Proc. of BPM 19, Springer LNCS, 2019.

• Implementation of MCMT.
  F. Alberti, S. Ghilardi, N. Sharygina A framework for the verification of parameterized infinite-state systems, In Proc. of CILC 14, CEUR, 2014.
  S. Ghilardi, S. Ranise MCMT: a Model Checker Modulo Theories, In Proc. of IJCAR'10, Springer LNCS, vol. 6173, pp. 22-29, 2010.
  S. Ghilardi, S. Ranise Model Checking Modulo Theory at work: the intergration of Yices in MCMT, Proc. of AFM 09, ACM Digital Library.

• Case Studies.
  F. Alberti, S. Ghilardi, E. Pagani, S. Ranise, G. Rossi BA: Automated Support for the Design and Validation of Fault Tolerant Parameterized Systems - a case study, Proc. of the XXIV DIStributed Computing Conference (DISC 10), Springer LNCS, 2010.
  A. Carioni, S. Ghilardi, S. Ranise MCMT in the Land of Parameterized Timed Automata, In Proc. of VERIFY 2010, co-located with IJCAR, Edinburgh, UK, (2010).
  R. Bruttomesso, A. Carioni, S. Ghilardi, S. Ranise Automated Analysis of Parametric Timing Based Mutual Exclusion Protocols, In Proc. the Fourth NASA Formal Methods Symposium, Norfolk, VA, USA (2012).