|
The
CAVA
Automata
Library
Title: |
The CAVA Automata Library |
Author:
|
Peter Lammich
|
Submission date: |
2014-05-28 |
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. |
BibTeX: |
@article{CAVA_Automata-AFP,
author = {Peter Lammich},
title = {The CAVA Automata Library},
journal = {Archive of Formal Proofs},
month = may,
year = 2014,
note = {\url{http://isa-afp.org/entries/CAVA_Automata.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
DFS_Framework, Flow_Networks, Formal_SSA, Gabow_SCC, LTL_to_GBA, Promela |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|