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, but since 2007 it is mainly developped by the LRDE, with some occasional collaborations with LIP6.

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 functional, and as long as you do not rely on the C++ API you should be fine in using this version. The C++ API is still due some important changes, so we recommend not upgrading to it yet if you have some code compatible with 1.2.x.

LRDE publications related to Spot

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