lurch092506.tar.gz

Lurch is a tool for exploring the behavior of a finite-state concurrent system. Lurch looks for violations of the same kind of properties a model checker (e.g., Gerard Holzmann's SPIN model checker) could be used to verify Unlike a model checker, however, Lurch uses a partial, random search of the space of system behaviors. The search is partial because Lurch is not guaranteed to explore the entire space of behaviors; the search is random in that the choice of which behaviors to explore is non-deterministic.

Lurch generally requires much less memory than a model checker, and often property violations are found faster, although Lurch's speed varies from one run to the next. On the other hand, Lurch does not perform an exhaustive search of the space of system behaviors, so Lurch should be thought of as a supplement, not a substitute, for model checking where there is enough time and memory for both.

Lurch Input Models
Basic Installation and Example Runs
Temporal Logic Properties