Project Overview

MMC (Mobility Model Checker) 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 the XSB 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 checking include the following: