MCMT is distributed "as is" without warranty of any kind; it is free for non-commercial
use. It is possible
the executables for
Linux (both 32/64 bit) and for Mac OS X together with some examples.
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
We run MCMT on four groups of examples:
the first and the second group comprise classical parametrized mutual exclusion and cache coherence protocols,
the third group some standard imperative programs, and the fourth group includes rather disparate examples
from various sources, aiming at showing 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 are available
Further case studies have been analyzed:
Parameterized Timed Systems:
benchmarks and statistics in this area (Fischer mutual exclusion, csma, etc.)
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 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, with additional abstraction/refinement features.
We thank R. Bruttomesso for supplying a parser that has been integrated in the current distribution; we also thank F. Alberti for the developement of
translation facilities from higher level specification languages.
S. Ghilardi, E. Nicolini,
S. Ranise, and
D. Zucchelli. Towards
SMT Model-Checking of Array-based Systems In Proc. of IJCAR'08
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.
Technique for invariant synthesis.
S. Ghilardi and
S. Ranise. Goal-directed Invariant
Synthesis for Model Checking Modulo Theories In Proc. of Tableaux 2009, Springer LNCS
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), to appear.
First Techniques for controlling symbolic state-space explosion.
S. Ghilardi, T. Valsecchi, and
S. Ranise. Light-Weight
SMT-based Model Checking In Proc. of
AVoCS'08, Elect. Notes in TCS (Extended
Implementation of MCMT.
MCMT: a Model Checker Modulo Theories,
In Proc. of IJCAR'10, Springer LNCS, to appear.
S. Ghilardi, S. Ranise
Model Checking Modulo Theory
at work: the intergration of Yices in MCMT, Proc. of AFM 09, ACM Digital Library.
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;
full version to appear in the Proc. of the 10th Int.
Work. on Automated Verification of Critical Systems (AVOCS 10), Electr. Communications of the EASST, vol.X, 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).