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 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 Seventh 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 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) —
- Publication Heuristics for Checking Liveness Properties with Partial Order Reductions in Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16) —
- Publication Spot 2.0 — a framework for LTL and ω-automata manipulation in Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA'16) —
- Publication Variations on Parallel Explicit Model Checking for Generalized Büchi Automata in International Journal on Software Tools for Technology Transfer (STTT) —
- Publication SAT-based Minimization of Deterministic ω-Automata in Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15) —