Michael Weber: Random Bits and Pieces

If we knew what it was we were doing, it would not be called research, would it?

Albert Einstein

New Paper

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


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)