Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - A Fully Verified Executable LTL Model Checker

Reference:

Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. Archive of Formal Proofs, May 2014. Formal proof development.

Suggested BibTeX entry:

@article{CAVA_LTL_Modelchecker-AFP,
    author = {Javier Esparza and Peter Lammich and Rene Neumann and Tobias Nipkow and Alexander Schimpf and Jan-Georg Smaus},
    journal = {Archive of Formal Proofs},
    month = {May},
    note = {Formal proof development},
    title = {A Fully Verified Executable {LTL} Model Checker},
    year = {2014}
}

See afp.sourceforge.net ...