TY - GEN
T1 - HARE
T2 - 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
AU - Roohi, Nima
AU - Prabhakar, Pavithra
AU - Viswanathan, Mahesh
N1 - Funding Information:
We gratefully acknowledge the support of the following grants-Nima Roohi was partially supported by NSF CNS 1329991; Pavithra Prabhakar was partially supported by NSF CAREER Award 1552668; and Mahesh Viswanathan was partially supported by NSF CCF 1422798 and AFOSR FA9950-15-1-0059.
Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017
Y1 - 2017
N2 - HARE (Hybrid Abstraction-Refinement Engine) is a counterexample 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 polyhedral 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, andC2E2).
AB - HARE (Hybrid Abstraction-Refinement Engine) is a counterexample 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 polyhedral 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, andC2E2).
UR - http://www.scopus.com/inward/record.url?scp=85017511022&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85017511022&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-54577-5_33
DO - 10.1007/978-3-662-54577-5_33
M3 - Conference contribution
AN - SCOPUS:85017511022
SN - 9783662545768
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 573
EP - 588
BT - Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
A2 - Margaria , Tiziana
A2 - Legay, Axel
PB - Springer
Y2 - 22 April 2017 through 29 April 2017
ER -