LTSmin: Distributed and Symbolic Reachability (tool paper accepted for publication to CAV 2010).

Abstract

In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems. These models are typically generated from specifications in high-level languages. The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to archive the resulting labelled transition systems (LTSs), and to minimize them with respect to (branching) bisimulation.

This is a tool paper; a companion technical report provides more details on the methods (its sections on features and benchmarking are by now outdated):
Stefan Blom, Jaco van de Pol and Michael Weber. Bridging the Gap between Enumerative and Symbolic Model Checkers, Technical Report TR-CTIT-09-30, CTIT, University of Twente, Enschede. (2009)

An Embeddable Virtual Machine for State Space Generation, International Journal on Software Tools for Technology Transfer (STTT), DOI: 10.1007/s10009-010-0141-2.

Abstract

The semantics of modelling languages are not always specified in a precise and formal way, and their rather complex underlying models make it a non-trivial exercise to reuse them in newly developed tools. We report on experiments with a virtual machine-based approach for state space generation. The virtual machine's (VM) byte-code language is straightforwardly implementable, facilitates reuse and makes it an adequate target for translation of higher-level languages like the SPIN model checker's PROMELA, or even C. As added value, it provides efficiently executable operational semantics for modelling languages. Several tools have been built on top of the VM implementation we developed, to evaluate the benefits of the proposed approach.

(Invited journal version of an earlier SPIN publication.)

It is downright scary how accurately PhD comics keep documenting my life:

(I am on holidays all of December to play with my Little One, during the day. Which effectively means that I work from home and at night four days per week, and only go one day per week to university... Oh well. Did I mention the guy in the comic is named Mike?)

UPDATE 2010-01-14: Two More...

We have released version 1.5 of LTSmin. The following improvements have been implemented:

• New frontend DVE (requires DiVinE-cluster)
• Bignum support for state counts in spec-reach tools
  (Jeroen Ketema)
• spec-reach clean-up
• 'tree' vector set implementation based on AtermDD

The source code, installation instructions and manuals are available online:

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.4.

Mikel Evins has released Apis, a sample Common Lisp Cocoa application using CCL's Cocoa bridge. Obligatory screenshot:

For what it's worth, Mikel also provides Atta, which is a similar project but based on Gambit Scheme.