Spot

Spot is an object-oriented model checking library written in C++. It offers a set of bricks to experiment with and develop your own model checker based on transition-based generalized Büchi automata.

Spot was born in the MoVe team at LIP6 and is now developped by the LRDE.

The current stable version of Spot (1.2.x) is available from http://spot.lip6.fr/. However the current development version has so many major changes (including important changes to the API, now written in C++11, support for arbitrary omega-acceptance conditions, support for the Hanoi Omega Automata Format, command-line tools for automata manipulation, better Python bindings) that the next version will be called Spot 2.0 once it is polished enough. The current development version is fully functionnal, and as long as you do not rely on the C++ API (which is still due some important changes) you should be safe in using it.

LRDE publications related to Spot

• {{{2}}} — {{{3}}}
• {{{2}}} — {{{3}}}
• {{{2}}} — {{{3}}}
• {{{2}}} — {{{3}}}
• {{{2}}} — {{{3}}}
• {{{2}}} — {{{3}}}