Welcome to MMC!

The Mobility Model Checking Project
Stony Brook Computer Science

Mobility Model Checker (MMC) is a model checker for verifying mobile systems specified in the style of the pi-calculus and properties specified using a subset of the pi-mu-calculus. The pi-calculus is a process algebra that can model mobile systems whose interconnections change dynamically, as opposed to static systems with just a fixed communication topology. MMC is build upon the XSB tabled logic programming system (developed by Stony Brook).

Stony Brook