An Optimizing Compiler for the pi-calculus

We developed an optimizing compilation technique which transforms high-level pi-calculus specifications into rules from which transitions of the global automata can be efficiently generated without requiring user's annotation. Our compiler uses a compact state representation and pre-computes the synchronizations in polynomial time during compilation while generating transitions during verification. We have also developed an AC-matching based symmetry reduction technique to recognize states that are equivalent due to symmetry, thereby reducing state space traversed during model checking. The compiler reduces both time and memory requirements of MMC by up to an order of magnitude.