SpaceEx State Space Explorer


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.

PHAVer Web Site