##
A Provably Correct Compiler for Efficient Model Checking of Mobile Processes

We present an optimizing compiler for the pi-calculus that significantly
improves the time and space performance of the MMC model checker.
MMC exploits the similarity between the manner in which resolution techniques
handle variables in a logic program and the manner in which the operational
semantics of the pi-calculus handles names by representing pi-calculus
names in MMC as Prolog variables, with distinct names represented by
distinct variables. Given a pi-calculus process P, our compiler for MMC
produces an extremely compact representation of P's symbolic state space as a
set of transition rules. It also uses AC unification to recognize
states that are equivalent due to symmetry.