Recent developments in theory and tool support for hybrid systems verification with HyPro

Abstract

Over the last decades, the development of algorithms and tools for the safety verification of hybrid systems has been content of intensive research. Numerous novel ideas have been presented and implemented in different tools. Whereas the majority of these tools offer fixed implementations, only few general libraries have been provided for the development of new verification tools. HYPRO is such an example, providing a C++ programming library for the implementation of certain types of reachability analysis algorithms for linear hybrid systems. These algorithms, based on flowpipe construction, need geometric or symbolic representation for state sets of hybrid systems. HYPRO offers datatypes for different representations, conversions between them, and efficient algorithms based on these datatypes. Since its release in 2017, HYPRO's functionalities have been extended by several implementations. In this paper we give a general introduction to flowpipe-construction-based methods and report on HYPRO's functional advances as well as on applications of the library.