Matthias Horbach

Hierarchical Analysis of Hybrid Automata

The verification tool HAHA (Hierarchical Analysis of Hybrid Automata) implements an algorithm for safety verification of unbounded uniform systems of linear automata. It employs an extension of the hierarchical theorem prover H-PILoT to reduce the verification problem to ground satisfiability problems in the base theory of linear real arithmetic with free function symbols. These problems are then checked by an SMT prover.


We use an XML format to describe hybrid automata, or families thereof. To analyze an automaton, execute the following command:

The following command line options are available:


The development version of the tool and its sources are available upon request.

We collected the raw data for the experiments described in our submitted paper in a tgz archive in May 2015. This archive contains

All executables are included in a windows variant (.exe) as well as a unix variant.

Available downloads: