MCMT: Model Checker Modulo Theories

Last Release: version 2.5.2 -- Last Update: 18/6/2015

MCMT is a model checker for infinite state systems based on the integration of Satisfiability Modulo Theories (SMT) solving and backward reachability. In its actual implementation, MCMT is capable of model checking invariant (safety) properties of a large class of infinite state systems called array-based systems.

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 (both 32/64 bit) and for Mac OS X together with some examples. The executables for the old versions 2.0 and 1.1.1 are still here and 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 solver Yices.

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: benchmarks and statistics in this area (Fischer mutual exclusion, csma, etc.) are available here;

  • Mutual exclusion, deadlock freedom and waiting time bounds for Fischer and Lynch-Shavit algorithms: see here for full analysis, statistics and benchmarks;

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

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

Related Tools

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.

The tools ArCa and ArCa_Sat analyze model-checking and satisfiability problems involving arrays and cardinality constraints; see here for more information.

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

Aknowledgements

We thank R. Bruttomesso for supplying a parser that has been integrated in the current distribution; we also thank F. Alberti for various help and for the developement of translation facilities from higher level specification languages.

Main Publications