Reference:

Javier Esparza, Peter Lammich, Rene Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In CAV, pages 463–478, 2013.

Suggested BibTeX entry:

@inproceedings{DBLP:confcavEsparzaLNNSS13,
    author = {Javier Esparza and Peter Lammich and Rene Neumann and Tobias Nipkow and Alexander Schimpf and Jan-Georg Smaus},
    booktitle = {CAV},
    pages = {463-478},
    title = {A Fully Verified Executable {L}{T}{L} Model Checker},
    year = {2013}
}