Abstract
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 language | Unknown |
|---|---|
| Publisher | Unknown Publisher |
| Publication status | Published - 1 Jan 2009 |