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.
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) —