| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
A Fully Verified Executable LTL Model Checker
| Title: | A Fully Verified Executable LTL Model Checker |
| Authors: | Javier Esparza, Peter Lammich, René Neumann (rene /dot/ neumann /at/ in /dot/ tum /dot/ de), Tobias Nipkow, Alexander Schimpf (schimpfa /at/ informatik /dot/ uni-freiburg /dot/ de) and Jan-Georg Smaus |
| Submission date: | 2014-05-28 |
| 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.
An early version of this model checker is described in the CAV 2013 paper with the same title. |
| BibTeX: |
@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},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |