Polyhedral Hybrid Automaton Verifyer
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.
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
(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.
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 source code, v. 0.38
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.
A. Fehnker and F. Ivancic, Benchmarks for Hybrid System Verification. Proc. HSCC 2004, Philadelphia, Springer, 2004. http://www.ece.cmu.edu/~ansgar/benchmark/
- Mutual Exclusion Protocol
- Bouncing Ball
- Stiff Oscillator
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)
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
Hybrid Systems Tools Wiki
This great collection of hybrid system tools by George Pappas has rendered my own list obsolete.
A library for exact computations with non-convex polyhedra, written in C++ but with interfaces to other languages..