A Fully Verified Executable LTL Model Checker
We present an LTL model checker whose code has been completely
verified using the Isabelle theorem prover. The checker consists of
over 4000 lines of ML code. The code is produced using recent Isabelle
technology called the Refinement Framework, which allows us to split
its correctness proof into (1) the proof of an abstract version of the
checker, consisting of a few hundred lines of ``formalized
pseudocode'', and (2) a verified refinement step in which mathematical
sets and other abstract structures are replaced by implementations of
efficient structures like red-black trees and functional arrays. This
leads to a checker that, while still slower than unverified checkers,
can already be used as a trusted reference implementation against
which advanced implementations can be tested. We report on the
structure of the checker, the development process, and some
experiments on standard benchmarks.
pdf
BibTeX:
@inproceedings{EsparzaLNNSS-CAV13,
author={Javier Esparza and Peter Lammich and Ren\'{e} Neumann
and Tobias Nipkow and Alexander Schimpf and Jan-Georg Smaus},
title={A Fully Verified Executable LTL Model Checker},
booktitle={Computer Aided Verification (CAV 2013)},
editor={N. Sharygina and H. Veith},
publisher=Springer,series=LNCS,volume=8044,pages={463-478},year=2013}
AFP entry with Isabelle theories.
Depends on a number of other AFP entries.
The CAV paper describes an early version.
Project home page