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}
}