Difference between revisions of "Spot"
From LRDE
Tag: Undo |
|||
(10 intermediate revisions by 5 users not shown) | |||
Line 8: | Line 8: | ||
<!-- |
<!-- |
||
this text was included in Projects.WebHome and Lrde.AreaOfExpertise |
this text was included in Projects.WebHome and Lrde.AreaOfExpertise |
||
− | Be careful with the wiki word : use [[Spot.WebHome]] instead of |
+ | Be careful with the wiki word : use [[Spot.WebHome]] instead of Spot |
--> |
--> |
||
<!-- SPOTINTROSTART --> |
<!-- SPOTINTROSTART --> |
||
Line 14: | Line 14: | ||
based on transition-based generalized Büchi automata. |
based on transition-based generalized Büchi automata. |
||
− | Spot was born in the [http://www.lip6.fr/fr/recherche/team.php?id=720 |
+ | Spot was born in the [http://www.lip6.fr/fr/recherche/team.php?id=720 MoVe team] at [http://www.lip6.fr/ LIP6], but since 2007 it is mainly developped by the LRDE, with some occasional collaborations with LIP6. |
<!-- SPOTINTROSTOP --> |
<!-- SPOTINTROSTOP --> |
||
+ | Please go to [https://spot.lrde.epita.fr/ Spot's website] for further information. |
||
− | The Spot website: http://spot.lip6.fr/ |
||
− | + | <br> |
|
+ | |||
+ | == LRDE publications related to Spot == |
||
+ | |||
+ | {{#ask: [[Category:SpotNews]] OR [[Category:Publications]] [[Published has news::true]] [[Related project::Spot]] |
||
+ | | ?News title=title |
||
+ | | ?News subtitle=subtitle |
||
+ | | ?News date#MEDIAWIKI=date |
||
+ | | format = ul |
||
+ | | template = ShortNewsItem |
||
+ | | order = descending |
||
+ | | sort = News date |
||
+ | | limit = 10 |
||
+ | | searchlabel = |
||
+ | }} |
Latest revision as of 10:27, 29 July 2022

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 Towards Better Heuristics for Solving Bounded Model Checking Problems in Constraints —
- Publication Tuning SAT Solvers for LTL Model Checking in Proceedings of the 29th Asia-Pacific Software Engineering Conference (APSEC'22) —
- Publication Go2Pins: A framework for the LTL verification of Go programs (Extended Version) in International Journal on Software Tools for Technology Transfer (STTT) —
- Publication Energy Problems in Finite and Timed Automata with Büchi Conditions in International Symposium on Formal Methods (FM) —
- Publication From Spot 2.0 to Spot 2.10: What's New? in Proceedings of the 34th International Conference on Computer Aided Verification (CAV'22) —
- Publication LTL under reductions with weaker conditions than stutter invariance in Proceedings of the 41th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE'22) —
- Publication Practical Applications of the Alternating Cycle Decomposition in Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'22) —
- Publication Towards Better Heuristics for Solving Bounded Model Checking Problems in Proceedings of the 27th International Conference on Principles and Practice of Constraint Programmings (CP'21) —
- Publication A Portable, Simple, Embeddable Type System in Proceedings of the 14th European Lisp Symposium (ELS) —
- Publication Improving swarming using genetic algorithms in Innovations in Systems and Software Engineering: a NASA journal (ISSE) —