is a model checker for mobile systems specified
in the style of the pi-calculus. MMC addresses the salient issues that
arise in the pi-calculus including scope extrusion and intrusion, and
dynamic generation of new names to avoid name capture. MMC also supports
verification of security protocols specified using spi-calculus.
MMC has been evolved from a model checker to a comprehensive toolset that
consists of a user specification language, a
compiler, a model checker, and a justifier.
The MMC environment builds on
tabled logic programming system developed at the Department of Computer Science
at Stony Brook University.
The anticipated benefits from a logic programming-based approach to model
A specification of a model checker is given at the level of semantic
equations, and is therefore not limited to any specific system specification
language or logic.
XSB is essentially a deductive system for proving theorems
in Horn logic. Moreover,
XSB meta-interpreters can be used to execute arbitrary deductive
Hence, the logic programming-based approach offers a unique opportunity
to fully and flexibly integrate aspects of verification based
on deduction, such as induction, to
approaches to model checking.
The state spaces of systems modeled in the pi-calculus is unbounded since
process may generate new channels dynamically, choosing names from an infinite
By using constraints to finitely represent infinite sets and
tabled resolution to efficiently compute fixed points over these sets,
tabled (contraint) LP is an effective approach for verifying infinite state
The high level at which model checking is specified correspondingly elevates
the level at which erroneous system specifications can be diagnosed and
The ability of a tabled LP system to execute directly and efficiently program analyses
facilitates the incorporation of process and formula
abstractions. Such abstractions are based on Abstract Interpretation
techniques, which have been used successfully to ameliorate the
state space explosion problem in model checking.
The programmability of a tabled LP system allows for direct encoding of traditional
model checking optimizations such as partial order reduction.