### Abstract

We report on the graph and automata library that is used in the fully verified LTL model checker CAVA. As most components of CAVA use some type of graphs or automata, a common automata library simplifies assembly of the components and reduces redundancy.

The CAVA Automata Library provides a hierarchy of graph and automata classes, together with some standard algorithms. Its object oriented design allows for sharing of algorithms, theorems, and implementations between its classes, and also simplifies extensions of the library. Moreover, it is integrated into the Automatic Refinement Framework, supporting automatic refinement of the abstract automata types to efficient data structures.

Note that the CAVA Automata Library is work in progress. Currently, it is very specifically tailored towards the requirements of the CAVA model checker. Nevertheless, the formalization techniques presented here allow an extension of the library to a wider scope. Moreover, they are not limited to graph libraries, but apply to class hierarchies in general.

The CAVA Automata Library is described in the paper: Peter Lammich, The CAVA Automata Library, Isabelle Workshop 2014.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session CAVA_Base

- Statistics
- Code_String
- CAVA_Code_Target
- CAVA_Base
- Lexord_List
- All_Of_CAVA_Base

### Session CAVA_Automata

- Digraph_Basic
- Digraph
- Automata
- Lasso
- Simulation
- Step_Conv
- Stuttering_Extension
- Digraph_Impl
- Automata_Impl
- All_Of_CAVA_Automata

### Depends on

- Collections Framework
- Deriving class instances for datatypes

### Used by

- Flow Networks and the Min-Cut-Max-Flow Theorem
- A Framework for Verifying Depth-First Search Algorithms
- Verified Construction of Static Single Assignment Form
- A Fully Verified Executable LTL Model Checker
- Converting Linear-Time Temporal Logic to Generalized Büchi Automata
- Promela Formalization
- Verified Efficient Implementation of Gabow’s Strongly Connected Components Algorithm
- Collections Framework

## Cite

×

CAVA_Automata-AFP

    @article{CAVA_Automata-AFP,
      author  = {Peter Lammich},
      title   = {The CAVA Automata Library},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/CAVA_Automata.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- May 29, 2014 : Isabelle2013-2