Spatial Logic Model Checker is a tool that allows the user to automatically verify behavioral and spatial properties of distributed concurrent systems expressed in the pi-calculus of Milner, Parrow and Walker. The algorithm implemented (currently using on-the-fly model-checking techniques) is provably correct for all processes, and complete for the class of bounded processes, an abstract class of processes that includes the finite control fragment of the pi-calculus. The tool itself is written in OCaml, and runs on any platform supported by the OCaml distribution.
