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 (both 32/64 bit) and for Mac OS X together with some examples.

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 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 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 for more information.

Related Tools

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.

Aknowledgements

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.

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.

• 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 (extended version).

• 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 version).

• Implementation of MCMT.
  S. Ghilardi, S. Ranise 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.

• 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; 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).