Computer Aided Verification of Automata (CAVA). 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.

References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)

Further publications can be found at: