On behalf of my co-authors I am happy to announce that our submission “Recent Developments in Theory and Tool Support for Hybrid Systems Verification with HyPro” for the journal Information and Computation has been accepted for publication.
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 implementations for fixed algorithms, only few general libraries have been provided to support the development of new verification tools.
HyPro is such an example, providing a C++ programming library for the fast implementation of certain types of reachability analysis algorithms for linear hybrid systems. These algorithms, based on flowpipe construction, need some geometric or symbolic representation for state sets of hybrid systems. HyPro offers datatypes for different such representations, conversions between them, and some efficient algorithms based on these datatypes to demonstrate their usage and impact.
Since its first release in 2017, several datatypes and algorithmic extensions have been implemented to extend HyPro’s functionalities. In this paper we give a general introduction to flowpipe-construction-based methods and report on HyPro’s functional advances as well as on some applications of the library.