A Fully Verified Executable LTL Model Checker

Javier Esparza (1) , Peter Lammich (2) , René Neumann (2) , Tobias Nipkow (2) , Alexander Schimpf (3) , Jan-Georg Smaus (4)

1 LRR-TUM - Institut für Informatik
2 TUM - Technische Universität Munchen - Technical University Munich - Université Technique de Munich
3 University of Freiburg [Freiburg]
4 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées

Mots clés: Model checking; LTL; interactive theorem proving; Isabelle

Domaines: Informatique [cs]

Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, et al.. A Fully Verified Executable LTL Model Checker. [Research Report] Archive of Formal Proofs. 2016. ⟨hal-03172233⟩