AVERIST Algorithmic Verifier of Stability

The AVERIST tool is an algorithmic approach for stability analysis of hybrid systems. It is designed as a framework for counterexample guided abstraction refinement (CEGAR).

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.

  1. An algorithmic approach to stability verification of polyhedral switched systems, Pavithra Prabhakar and Miriam García Soto. American Control Conference (ACC), 2014.

  2. Abstraction based Model-Checking of Stability of Hybrid Systems, Pavithra Prabhakar and Miriam García Soto. Computer Aided Verification (CAV), 2013.