Downloads

Finite Automata Library

A snapshot of a formalisation of finite automata that is part of CAVA is available here:
  • Proof Document (738 KB, 6 Feb 2012)
  • Proof Outline (416 KB, 6 Feb 2012)
  • sources (1.5 MB, 13 Feb 2012) -- including some libraries from AFP as well as PolyML and OCaml code

DFS Framework

A snapshot of a formalized framework for depth-first search that is part of CAVA is available here:
  • Proof Document (458 KB, 12 Jun 2012)
  • Proof Outline (280 KB, 12 Jun 2012)
  • sources (6 MB, 12 Jun 2012) -- including some libraries from AFP, SML/OCaml/Haskell code and example automata

Supporting Material CAV13

This is located at an extra page.

Supporting Material CAVA with Partial Order Reduction

This is located at an extra page.