Spot
From LRDE
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.
Please go to Spot's website for further information.
- Publication A Portable, Simple, Embeddable Type System in European Lisp Symposium —
- Publication Improving swarming using genetic algorithms in Innovations in Systems and Software Engineering: a NASA journal (ISSE) —
- Publication LTL Model Checking for Communicating Concurrent Programs in Innovations in Systems and Software Engineering: a NASA journal (ISSE) —
- Publication Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization in Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20) —
- Publication Combining Parallel Emptiness Checks with Partial Order Reductions in Proceedings of the 21st International Conference on Formal Engineering Methods (ICFEM'19) —
- Publication Model checking with generalized Rabin and Fin-less automata in International Journal on Software Tools for Technology Transfer —
- Publication Improving Parallel State-Space Exploration Using Genetic Algorithms in Proceedings of the 12th International Conference on Verification and Evaluation of Computer and Communication Systems (VECOS'18) —
- Publication Reactive Synthesis from LTL Specification with Spot in Proceedings of the 7th Workshop on Synthesis, SYNT@CAV 2018 —
- Publication Parallel Model Checking Algorithms for Linear-Time Temporal Logic in Handbook of Parallel Constraint Reasoning —
- Publication CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving in Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18) —