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 Performance Comparison of Several Folding Strategies in Trends in Functional Programming —
- 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) —
- Publication Parallel Learning Portfolio-Based Solvers in Proceedings of the International Conference on Computational Science (ICCS) —
- Publication Explicit State Model Checking with Generalized Büchi and Rabin Automata in Proceedings of the 24th International SPIN Symposium on Model Checking of Software (SPIN'17) —
- Publication Seminator: A Tool for Semi-Determinization of Omega-Automata in Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-21) —