PHAVer

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:

• 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.

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

• (a) Library installation script, (many thanks to Flavio Lerda)
  - Downloads libraries (GMP, PPL) and compiles them.
  - Libraries will reside in ~/local, or as specified.
  - Type "sh build-libraries.sh" for information on usage.

• (b) PHAVer installation script, (many thanks to Flavio Lerda)
  - Requires the completion of (a), i.e., the libraries to be installed in ~/local.
  - Downloads PHAVer the source code and compiles it.
  - The binary phaver will reside in ~/local/bin.
  - To complete the installation, it is necessary to add ~/local/bin to the path or link to ~/local/bin/phaver.
  - The compilation is static, i.e., the libraries may be deleted afterwards.

• (c) For Mac OS X, there is a special version (kindly provided by Franck Cassez)
  - Library installation script
  - PHAVer installation script
  - PHAVer sources
  - installation guide
- a small patch for OS X 10.6 (thanks to Paul Maier)

Method 2: Ready-to-Use Executables

• PHAVer executable for Linux, v. 0.38 (static compilation)
  - no installation of libraries (GMP and PPL) necessary
  - may or may not work on your system (due to missing OS components)

• PHAVer executable for Windows XP, v. 0.33 (compiled under Cygwin)
  - Requires cygwin.dll, available at www.cygwin.com.
  - Note that the Windows version is about 3x slower due to the cygwin.dll.

• PHAVer executable for Windows XP, v. 0.35 (compiled under Cygwin)
  - unstable version

Source Code

• PHAVer source code, v. 0.38

Recommended Utilities

• For visualization of 2-dimensional PHAVer output, we recommend "graph" of the plotutils package (also available under Cygwin).

• A script for visualizing 2-dimensional PHAVer output in MATLAB. It uses the same input format as graph.

• For recording memory consumption, we use the utility "memtime", which is available for download at www.uppaal.com.

Examples

• Navigation Benchmark from
  A. Fehnker and F. Ivancic, Benchmarks for Hybrid System Verification. Proc. HSCC 2004, Philadelphia, Springer, 2004. http://www.ece.cmu.edu/~ansgar/benchmark/

• Various Examples:
  - Mutual Exclusion Protocol
  - Bouncing Ball
  - Forward/backward-Refinement
  - Stiff Oscillator

Documentation

• Goran Frehse. PHAVer: Algorithmic Verification of Hybrid Systems past HyTech. Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC), Lecture Notes in Computer Science 3414, Springer-Verlag, 2005, pp. 258-273 (extended and revised) BibTeX (DBLP)

• PHAVer Language Overview v0.35

Contact

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

Acknowledgments

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.

Links

Verification Tools for Hybrid Systems

• Hybrid Systems Tools Wiki
  This great collection of hybrid system tools by George Pappas has rendered my own list obsolete.

Other Software

• Parma Polyhedra Library
  A library for exact computations with non-convex polyhedra, written in C++ but with interfaces to other languages..