Chapter 1
Introduction

HSolver is a software package for the formal verification of safety properties of continuous time hybrid systems over unbounded time. It allows hybrid systems with non-linear ordinary differential equations, and non-linear jumps. Even though it is based on fast machine-precision floating point arithmetic, it uses sound rounding, and hence the correctness of its results cannot be hampered by round-off errors. HSolver does not only verify safe hybrid systems, but—in addition—it also computes abstractions of the input system. So, even for input systems that are unsafe, or for which exhaustive formal verification is too difficult, it will compute abstractions that can be used by other tools. For example, the abstractions could be used for guiding search for error trajectories of unsafe systems. Efficiency improvements of the tool are guided by a continuously expanding database of benchmark examples.

HSolver currently is not yet optimized for special classes of hybrid systems (e.g., systems such as linear hybrid automata that have very simply continuous dynamics). Moreover it does not yet provide mature support for finding counter-examples for unsafe input systems.

The method used by HSolver is interval constraint propagation based abstraction refinement [3]. This method incrementally refines an abstraction of the input systems. Special care is taken to reflect as much information as possible into the abstraction without increasing its size.