Another Bisimulation Checker

Welcome to the homepage of ABC; the Advanced Bisimulation Checker. ABC is a tool that checks open-equivalence in the pi-calculus. Open bisimulation was first defined by Davide Sangiorgi. Roughly speaking, the ABC implements a small part of The Mobility Workbench of Björn Victor, but with some improvements. ABC has been used successfully for teaching here at EPFL.

You can download here the current distribution of ABC. You will need OCaml in order to compile ABC. The tool ledit made by Daniel de Rauglaudre could also be very useful. ABC should work on any good linux distribution. It should work also under the Cygwin environment and might work on MacOS X (provided that OCaml is present).

The User's Guide of ABC can be found in Postscript or PDF. You can browse here the examples that you can also find in the distribution.

Finally, feel free to get in touch with me if you have any comments/suggestions/whatever.