This is Enea.

Home

Personal Info

Research

Papers

Teaching

About

PHAVerLitePHAVerLite

[Page last updated on "November 03, 2022, 16:14:08".]

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 (and previous) versions

All the releases of PHAVerLite are available in the corresponding github page.

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 a high quality version of the image in this web page.

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 2011 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

We report the result of an experimental evalution, based on the benchmarks of the ARCH-COMP 2019 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.

Papers

  1. Anna Becchi and Enea Zaffanella
    Revisiting Polyhedral Analysis for Hybrid Systems
    Static Analysis - 26th International Symposium (SAS 2019) (Porto, Portugal, October 2019)
  2. Goran Frehse, Alessandro Abate, Dieky Adzkiya, Anna Becchi, Lei Bu, Alessandro Cimatti, Mirco Giacobbe, Alberto Griggio, Sergio Mover, Muhammad Syifa'Ul Mufid, Idriss Riouak, Stefano Tonetta, Enea Zaffanella
    ARCH-COMP19 Category Report: Hybrid Systems with Piecewise Constant Dynamics
    6th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH19) (Montreal, Canada, April 2019), EPiC Series in Computing.
© Enea Zaffanella
enea.zaffanella@unipr.it

| Home | Personal Info | Research | Papers | Teaching | About