Polyhedral Hybrid Automaton Verifyer

We highly recommend PHAVerLite as a successor to PHAVer.

PHAVer is a tool for verifying safety properies of hybrid systems. It stands out from other tools with the following features:

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.

Installation & Download

Latest Version: 0.38, Feb. 12, 2007

NEW: memory saving modes and reduced number of polyhedra!

Disclaimer: PHAVer is still in its early development stages. We apologize for any bugs, but can not assume any responsibility for the correctness of the results or any damages caused. The source code is available from the author upon request.

Please read the release notes: readme

Method 1: Using Installation Scripts

Method 2: Ready-to-Use Executables

Source Code

Recommended Utilities




For questions, suggestions or comments, please contact Goran Frehse under goran dot frehse at imag dot fr.


A big thanks to Franck Cassez for creating a version of PHAVer that compiles on Macs. Special thanks to Zulema Juarez, Gabriela Marin, Laurent Doyen, Li Hong and R.J.M. Theunissen for bug reports and helpful suggestions, and to Flavio Lerda for his invaluable compilation scripts. Many thanks also to Scott Little for his help with compilation problems. Finally, a big thanks goes to the PPL development team and in particular to Roberto Bagnara for his wonderful help.


Verification Tools for Hybrid Systems

Other Software