HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata

Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan

HARE (Hybrid Abstraction-Refinement Engine) is a coun- terexample guided abstraction-refinement (CEGAR) based tool to verify safety properties of hybrid automata, whose continuous dynamics in each mode is non-linear, but initial values, invariants, and transition relations are specified using linear constraints. HARE works by abstracting non- linear hybrid automata into hybrid automata with polyhedral inclusion dynamics, and uses dReach to validate counterexamples. We show that the CEGAR framework forming the theoretical basis of HARE, makes provable progress in each iteration of the abstraction-refinement loop. The current HARE tool is a significant advance on previous versions of HARE — it considers a richer class of abstract models (polyhedral flows as opposed to rectangular flows), and can be applied to a larger class of concrete models (non-linear hybrid automata as opposed to affine hybrid automata). These advances have led to better performance results for a wider class of examples. We report an experimental comparison of HARE against other state of the art tools for affine models (SpaceEx, PHAVer, and SpaceEx AGAR) and non-linear models (FLOW*, HSolver, and C2E2).

23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2017
Download: BIB PS PDF