CAVA is a DFG
-funded project that formalises and verifies important
algorithmic 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 indented to be used as a reference implementation.
For a detailed description
of the goals of the CAVA project, please have a look
at the Project Description