CAVA consists of the DFG projects Computer Aided Verification of Automata (completed) and Verified Model Checkers (ongoing). Its aim is the formalisation and verification of important parts of automata theory and model checking using the proof assistant Isabelle/HOL. While the algorithms are formalised on a mathematical, abstract level, they are still intended to be executable. The code that is automatically generated by Isabelle is intended to be used as a reference implementation.
The following groups participate in the CAVA project:
DFG Project Information: GEPRIS Entry
Duration: 2010 - 2019
Members: Julian Brunner (TUM), Javier Esparza (TUM), Peter Lammich (TUM), René Neumann (TUM), Tobias Nipkow (TUM), Alexander Schimpf (Uni Freiburg), Salomon Sickert (TUM, HUJI), Jan-Georg Smaus (IRIT), Thomas Tuerk (TUM)
The CAVA project aims at formalising and verifying important algorithmic parts of automata theory as well as its applications in model checking. These formalisations are done in higher order logic using the interactive theorem prover Isabelle. The algorithms are formalised on an mathematical, abstract level, using mainly sets and relations. At the same time these formalisations are intended to be executable. This means, that Isabelle is able to automatically generate programs in Haskell, OCaml or SML from these formalisations.
The generated programs are intended to be reference implementations that can be used to test the correctness of other implementations. Therefore, all algorithms that are needed for model checking have to be verified. Otherwise a mixture of verified and unverified components would undermine the trust in the reference implementation.
The goal is to formalise key algorithms of the fields of automata theory and model checking. Namely, the project formalises results for finite automata (on finite and infinite words), regular expressions, translations of linear temporal logic to ω-automata, language emptiness checks, and finite state model checking.
DFG Project Information: GEPRIS Entry
Duration: 2016 - now
Members: Julian Brunner (TUM), Javier Esparza (TUM), Jan Křetínský (TUM), Peter Lammich (TUM), Tobias Nipkow (TUM), Salomon Sickert (TUM, HUJI)
The first goal consists of developing an efficient (competitive) verified model checker for LTL. This is the continuation of the CAVA project with more ambitious goals: We want to improve our reference implementation which is 1-2 orders of magnitude slower than SPIN to be as efficient as SPIN while still being fully verified.
The second goal is to develop a verified probabilistic model checker for PLTL (probabilistic LTL), PCTL, and PCTL* which can be used as reference implementations. We want to model our implementation after the popular (unverified) probabilistic model checkers PRISM and MRMC. This is the merger of the CAVA and the PM (probabilistic model checking) project. The focus lies on transforming the mathematical foundation from the PM project into executable algorithms, although these may to yet be competitive with PRISM.
Members of the the projects reported their results in the following peer-reviewed publications.
Salomon Sickert
A Unified Translation of Linear Temporal Logic to ω-Automata
Dissertation (2019):
bibtex / view
René Neumann
CAVA - A Verified Model Checker
Dissertation (2017):
bibtex / view
Michael Luttenberger, Philipp J. Meyer, Salomon Sickert
Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games
Acta Informatica (2020):
bibtex / view / preprint
Julian Brunner, Peter Lammich
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
Journal of Automated Reasoning (2018):
bibtex / view
Javier Esparza, Jan Křetínský, Salomon Sickert
From LTL to deterministic automata - A safraless compositional approach
FMSD (2016):
bibtex / view
Salomon Sickert, Javier Esparza
An Efficient Normalisation Procedure for Linear Temporal Logic and Very Weak Alternating Automata
LICS (2020):
bibtex / view / preprint / λ formalisation / Java implementation
Peter Lammich
Generating Verified LLVM from Isabelle/HOL
ITP (2019):
bibtex / view
Julian Brunner, Benedikt Seidl, Salomon Sickert
A Verified and Compositional Translation of LTL to Deterministic Rabin Automata
ITP (2019):
bibtex / view / λ formalisation
Simon Wimmer, Peter Lammich
Verified Model Checking of Timed Automata
TACAS (2018):
bibtex / view
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
CAV (2018):
bibtex / view
Philipp Meyer, Salomon Sickert, Michael Luttenberger
Strix: Explicit Reactive Synthesis Strikes Back!
CAV (2018):
bibtex / view
Javier Esparza, Jan Křetínský, Salomon Sickert
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata
LICS (2018):
bibtex / view / preprint
Jan Křetínský, Tobias Meggendorfer, Salomon Sickert
Owl: A Library for ω-Words, Automata, and LTL
ATVA (2018):
bibtex / view
Javier Esparza, Jan Křetínský, Jean-Francois Raskin, Salomon Sickert
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
TACAS (2017):
bibtex / view / preprint
Julian Brunner, Peter Lammich
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
NFM (2016):
bibtex / view
Peter Lammich, René Neumann
A Framework for Verifying Depth-First Search Algorithms
CPP (2015):
bibtex / view
René Neumann
Using Promela in a Fully Verified Executable LTL Model Checker
VSTTE (2014):
bibtex / view / λ formalisation
Peter Lammich
Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
ITP (2014):
bibtex / view / λ formalisation
Peter Lammich
Automatic Data Refinement
ITP (2013):
bibtex / view / λ formalisation
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker
CAV (2013):
bibtex / view / λ formalisation
Peter Lammich, Thomas Tuerk
Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
ITP (2012):
bibtex / view
René Neumann
A Framework for Verified Depth-First Algorithms
ATX (2012):
bibtex / view
All major publications are usually accompanied by a formalisation that has been submitted to the Archive of Formal Proofs. Over the years the following entries have been submitted.
Salomon Sickert
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
Archive of Formal Proofs (2020):
bibtex / view
Benedikt Seidl, Salomon Sickert
A Compositional and Unified Translation of LTL into ω-Automata
Archive of Formal Proofs (2019):
bibtex / view
Julian Brunner
Partial Order Reduction
Archive of Formal Proofs (2018):
bibtex / view
Julian Brunner
Transition Systems and Automata
Archive of Formal Proofs (2017):
bibtex / view
Julian Brunner
Büchi Complementation
Archive of Formal Proofs (2017):
bibtex / view
Peter Lammich, René Neumann
A Framework for Verifying Depth-First Search Algorithms
Archive of Formal Proofs (2016):
bibtex / view
Salomon Sickert
Linear Temporal Logic
Archive of Formal Proofs (2016):
bibtex / view
Salomon Sickert
Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata
Archive of Formal Proofs (2015):
bibtex / view
Peter Lammich
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Archive of Formal Proofs (2014):
bibtex / view
Peter Lammich
The CAVA Automata Library
Archive of Formal Proofs (2014):
bibtex / view
Peter Lammich
Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm
Archive of Formal Proofs (2014):
bibtex / view
René Neumann
Promela Formalization
Archive of Formal Proofs (2014):
bibtex / view
Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, Jan-Georg Smaus
A Fully Verified Executable LTL Model Checker
Archive of Formal Proofs (2014):
bibtex / view
Peter Lammich
Automatic Data Refinement
Archive of Formal Proofs (2013):
bibtex / view