In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems. But due to practical and systematic
limitations it is only applicable to relatively simple systems. We address the main problems of HyTech with PHAVer, a new
tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives,
so-called linear hybrid automata. Affine dynamics are handled by on-the-fly overapproximation and partitioning of the state
space based on user-provided constraints and the dynamics of the system. PHAVer features exact arithmetic in a robust implementation
that, based on the Parma Polyhedra Library, supports arbitrarily large numbers. To force termination and manage the complexity
of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra.
Experimental results for a navigation benchmark and a tunnel diode circuit demonstrate the effectiveness of the approach.
Keywords Hybrid systems - Verification - Tools - Polyhedra
A preliminary version of this paper appeared in the Proceedings of Hybrid Systems: Computation and Control (HSCC 2005), Lecture Notes in Computer Science 3414, Springer-Verlag,
2005, pp. 258–273.