CAVA LTL Modelchecker

CAVA_LTL_Modelchecker: A Fully Verified Executable LTL Model Checker. 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.

References in zbMATH (referenced in 17 articles )

Showing results 1 to 17 of 17.
Sorted by year (citations)

  1. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano: Certifying proofs for SAT-based model checking (2021)
  2. Popescu, Andrei; Lammich, Peter; Hou, Ping: CoCon: a conference management system with formally verified document confidentiality (2021)
  3. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  4. Lammich, Peter: Refinement to imperative HOL (2019)
  5. Lammich, Peter; Lochbihler, Andreas: Automatic refinement to efficient data structures: a comparison of two approaches (2019)
  6. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  7. Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
  8. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2018)
  9. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  10. Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
  11. Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)
  12. Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco: CoSMed: a confidentiality-verified social media platform (2016)
  13. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  14. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  15. Aransay, Jesús; Divasón, Jose: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (2015)
  16. Noschinski, Lars: A graph library for Isabelle (2015)
  17. Esparza, Javier; Lammich, Peter; Neumann, René; Nipkow, Tobias; Schimpf, Alexander; Smaus, Jan-Georg: A fully verified executable LTL model checker (2013) ioport