PHAVer

PHAVer

Description: PHAVer (Polyhedral Hybrid Automaton Verifyer) 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 is now included in SpaceEx.

VO Integration: No

Active: No

Available Benchmarks: Yes. See "Examples" section of the webpage.

Website: http://www-verimag.imag.fr/~frehse/phaver_web/index.html

Download: See "Installation & Download" section of webpage.

Documentation: See "Documentation" section of webpage.

Contact: Goran Freshe

Excerpt and graphic from: http://www-verimag.imag.fr/~frehse/phaver_web/index.html