The AVERIST tool is an algorithmic approach for stability analysis of hybrid systems.
It is designed as a framework for counterexample guided abstraction refinement
Currently, the processes implemented are Abstraction and Model-checking.
A CEGAR loop consists of four phases: abstraction, model-checking, validation and refinement.
An abstraction of the original (concrete) system is constructed and model-checked,which either
results in a stability proof or an abstract counterexample indicating a potential reason for
instability. In the latter case, the abstract counterexample is analysed to either infer a bug
in the concrete system or construct a finer abstraction.