## 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.