PHAVer is a tool for verifying safety properies of hybrid systems. It stands out from other tools with the following features:
exact and robust arithmetic with unlimited precision
on-the-fly over-approximation of piecewise affine dynamics
improved algorithms and termination heuristics
support for compositional and assume-guarantee reasoning.
In its polyhedral computations, PHAVer uses the Parma Polyhedra Library (PPL), a library for exact computations with non-convex polyhedra, written in C++ and with interfaces to other languages.