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