The Spatial Logic Model Checker User's Manual v1.15

Research output: Book/ReportCommissioned report


The Spatial Logic Model Checker is a tool allowing the user to automatically verify behavioral and spatial properties of distributed and concurrent systems expressed in a pi-calculus. 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.
Original languageUnknown
PublisherUnknown Publisher
Publication statusPublished - 1 Jan 2009

Cite this