In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems – yet it has remained severely
limited in its applicability to more complex 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. Affine dynamics
are handled by on-the-fly overapproximation and by partitioning the state space based on user-definable constraints and the
dynamics of the system. PHAVer’s exact arithmetic is robust due to the use of the Parma Polyhedra Library, which supports
arbitrarily large numbers. To 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
show the effectiveness of the approach.