A Fully Verified Executable LTL Model Checker

Javier Esparza 🌐, Peter Lammich 🌐, René Neumann 📧, Tobias Nipkow 🌐, Alexander Schimpf 📧 and Jan-Georg Smaus 🌐

May 28, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for 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 the Isabelle 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.

License

BSD License

Topics

Related publications

Session SM_Base

Session SM

Session CAVA_Setup

Session CAVA_LTL_Modelchecker

Depends on

Cite

× 
@article{CAVA_LTL_Modelchecker-AFP,
  author  = {Javier Esparza and Peter Lammich and René Neumann and Tobias Nipkow and Alexander Schimpf and Jan-Georg Smaus},
  title   = {A Fully Verified Executable LTL Model Checker},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/CAVA_LTL_Modelchecker.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: