### 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

- Computer science/Automata and formal languages

### Related publications

- Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., & Smaus, J.-G. (2013). A Fully Verified Executable LTL Model Checker. Lecture Notes in Computer Science, 463–478. https://doi.org/10.1007/978-3-642-39799-8_31
- author's copy
- Projekt home page

### Session SM_Base

### Session SM

- LTS
- SOS_Misc_Add
- SM_Datastructures
- Gen_Scheduler
- Gen_Scheduler_Refine
- SM_Syntax
- SM_State
- SM_Cfg
- SM_Semantics
- Decide_Locality
- Type_System
- SM_Finite_Reachable
- Pid_Scheduler
- SM_LTL
- Gen_Cfg_Bisim
- Rename_Cfg
- SM_Visible
- SM_Pid
- SM_Variables
- SM_Indep
- SM_Sticky
- SM_POR
- SM_Ample_Impl
- SM_Wrapup

### Session CAVA_Setup

### Session CAVA_LTL_Modelchecker

- NDFS_SI_Statistics
- NDFS_SI
- CAVA_Abstract
- BoolProgs
- BoolProgs_Extras
- BoolProgs_LTL_Conv
- BoolProgs_Philosophers
- BoolProgs_ReaderWriter
- BoolProgs_Simple
- BoolProgs_LeaderFilters
- BoolProgs_Programs
- CAVA_Impl
- Mulog
- All_Of_Nested_DFS
- All_Of_CAVA_LTL_Modelchecker

### Depends on

- The CAVA Automata Library
- A Framework for Verifying Depth-First Search Algorithms
- Partial Order Reduction
- Stuttering Equivalence
- Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm
- Converting Linear-Time Temporal Logic to Generalized Büchi Automata
- Promela Formalization

### Auto-related entries

- The string search algorithm by Knuth, Morris and Pratt
- Root-Balanced Tree

## Cite

×

CAVA_LTL_Modelchecker-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- May 30, 2014 : Isabelle2013-2
- May 29, 2014 : Isabelle2013-2