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 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) —
- Publication Parallel Satisfiability Solver Based on Hybrid Partitioning Method in Proceedings of the 25th Euromicro International Conference on Parallel, Distributed and Network-based Processing (PDP) —
- 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) —