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 swarming using genetic algorithms in Innovations in Systems and Software Engineering: a NASA journal (ISSE) —
- Publication LTL Model Checking for Communicating Concurrent Programs in Innovations in Systems and Software Engineering: a NASA journal (ISSE) —
- Publication Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-Determinization in Proceedings of the 32nd International Conference on Computer-Aided Verification (CAV'20) —
- 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) —