TY - GEN

T1 - A fully verified executable LTL model checker

AU - Esparza, Javier

AU - Lammich, Peter

AU - Neumann, René

AU - Nipkow, Tobias

AU - Schimpf, Alexander

AU - Smaus, Jan Georg

N1 - Funding Information:
Research supported by DFG grant CAVA, Computer Aided Verification of Automata.

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84881159117&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39799-8_31

DO - 10.1007/978-3-642-39799-8_31

M3 - Conference contribution

AN - SCOPUS:84881159117

SN - 9783642397981

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 463

EP - 478

BT - Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings

T2 - 25th International Conference on Computer Aided Verification, CAV 2013

Y2 - 13 July 2013 through 19 July 2013

ER -