The CAVA Automata Library

ABSTRACT. We report on the graph and automata library that is used in the fully verified LTL model checker CAVA. Most components of CAVA use some type of graphs or automata.

A common automata library simplifies assembly of the components to a working model checker 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 the different types of graphs, and also simplifies adding new graph types. 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 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.