PHAVerLite

PHAVerLite (PHAVer + PPLite) is a variant of PHAVer, a formal verification tool for computing reachability of hybrid systems.

The main difference with respect to PHAVer, originally developed by Goran Frehse and later included as a plugin in the SpaceEx platform, is the replacement of the Parma Polyhedra Library (PPL) with PPLite, a software library exploiting novel representations and algorithms for the manipulation of polyhedra.

Current version

• 2024-04-12: PHAVerLite 0.7 can be downloaded.
  This is based on PPLite 0.12. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 5.15.0-101.
• Links to all versions released.

Usage example

Try command phaverlite -v256001 osc_demo.pha.
File osc_demo.pha contains the hybrid model, the configuration commands and (commented out) the graph utility command needed to produce an image of the computed reachable set.

Building from sources

PHAVerLite is currently developed on a Linux system. In order to build it from sources the following dependencies need to be satisfied (see file README):

• a C++ compiler supporting the 2017 standard (e.g., g++ or clang++);
• reasonably recent versions of flex and bison;
• reasonably recent versions of numeric libraries GMP, MPFR and FLINT;
• a specific version of the PPLite library.

While not strictly a requirement, we suggest to install the graphviz tools to allow graphical display of the generated output.

Experimental evaluation

PHAVerLite took part to several editions of the ARCH-COMP friendly competition.

Support

If you need help for using PHAVerLite, ask me.

Here are a few notes on PHAVerLite's specification language.

Features

PHAVerLite currently provides a subset of the functionalities offered by PHAVer, focusing on automata where:

• state variable are continuous;
• each location invariant is a finite set of rational, convex, NNC (not necessarily topologically closed) polyhedra;
• each discrete transition between locations is a convex linear predicate on pre/post values of the state variables;
• the continuous dynamics at locations is modeled by piecewise constant bounds on the derivatives of state variables.

Note that some of the PHAVer functionalities (e.g., the computation of simulation relations) have been deliberately removed, whereas a few of the design and implementation choices have been (or are being) reconsidered. While being heavily based on the original PHAVer, PHAVerLite source code is being rewritten in modern C++, so as to simplify both maintenance and experimentation with novel algorithms and design tradeoffs. The developers should feel free to use language features made available by the recent standards, provided these lead to a simpler implementation or improve on code readability.

Development team

As said above, the starting point for the project was the source code of PHAVer, developed by Goran Frehse. The following people have contributed to the project:

• Enea Zaffanella (main developer, supervisor)
• Anna Becchi (contributor, former student)
• Idriss Riouak (contributor, former student)

Besides writing/improving PHAVerLite source code, contributions to the project include the design and implementation of a few ad-hoc algorithms on NNC polyhedra (thereby improving PPLite) and the development of a stand-alone tool for translating SpaceEx models into PHAVer syntax.

---

Available downloads

Note: older versions are no longer maintained; we highly recommend to switch to the most recent one.

• 2024-04-12: PHAVerLite 0.7 can be downloaded.
  This is based on PPLite 0.12. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 5.15.0-101.
• 2023-05-29: PHAVerLite 0.6 can be downloaded.
  This is based on PPLite 0.10.2. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 5.15.0-72.
• 2022-11-03: PHAVerLite 0.5 can be downloaded.
  This is based on PPLite 0.8. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 5.4.0-131-generic.
• 2020-11-24: PHAVerLite 0.4 can be downloaded.
  This is based on PPLite 0.7. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-123.
• 2020-06-15: PHAVerLite 0.3.1 can be downloaded.
  This fixes a bug in version 0.3 (no other changes). For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-106.
• 2020-04-23: PHAVerLite 0.3 can be downloaded.
  This is based on PPLite 0.6. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-96.
• 2019-10-17: PHAVerLite 0.2.1 can be downloaded.
  This is based on PPLite 0.5.1, which fixes a bug that may be affecting the computation of discrete transitions. For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-65.
• 2019-07-12: PHAVerLite 0.2 can be downloaded.
  For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-54.
• 2019-03-08: PHAVerLite 0.1 can be downloaded.
  For convenience, we also distribute the (gzipped) statically linked executable for x86_64 machines, built on Linux 4.15.0-46; this may work on other reasonably recent Linux distributions as well.

---

PHAVerLite's specification language

PHAVerLite inherits most of the specification language of PHAVer.

A few of the language commands and parameters of PHAVer are not supported; also, a few parameters have been subject to renaming in an attempt to somehow improve consistency. Here is a brief summary of the main changes.

• PHAVer's keywords do, end, goto, sync, wait are treated as identifiers in PHAVerLite; hence, they can be used as location names and/or syncronization label names without causing a syntax error.
• Parameter USE_CONVEX_HULL has been renamed to REACH_USE_CONVEX_HULL.
• Added parameter REACH_USE_CONSTRAINT_HULL.
• Parameter CHEAP_CONTAIN_RETURN_OTHERS has been renamed to REACH_CHEAP_CONTAINS.
• Added parameter REACH_CHEAP_CONTAINS_USE_BBOX.
• Parameter ELAPSE_TIME has been renamed to REACH_USE_TIME_ELAPSE.
• Parameter SEARCH_METHOD has been changed to only accept 3 values (rather than the 8 values accepted by PHAVer):
  • value 0: transaction based (corresponding to value 0 in PHAVer);
  • value 1: topological sort of all states (corresponding to value 7 in PHAVer);
  • value 2: topological sort of reachable states (corresponding to value 6 in PHAVer); this is the value used by default.
• Parameter REACH_ONLY_EXPLORE has been removed.
• Parameter REFINE_LOCATION_PLANE has been removed.
• All parameters related to simulation checking have been removed (as simulation checking is no longer supported).