The CAVA Project

Overview

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 Projects

Computer Aided Verification of Automata

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.

Verified Model Checkers

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.

Publications

Members of the the projects reported their results in the following peer-reviewed publications.

Disserations

Journals

Conferences & Workshops

Formalisations

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.