A fully verified executable LTL model checker

Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan Georg Smaus

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

68 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 25th International Conference, CAV 2013, Proceedings
Pages463-478
Number of pages16
DOIs
StatePublished - 2013
Event25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation
Duration: 13 Jul 201319 Jul 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8044 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Computer Aided Verification, CAV 2013
Country/TerritoryRussian Federation
CitySaint Petersburg
Period13/07/1319/07/13

Fingerprint

Dive into the research topics of 'A fully verified executable LTL model checker'. Together they form a unique fingerprint.

Cite this