PHAVerLite: experimental evaluation

PHAVerLite (version 0.1) participated to the ARCH-COMP 2019 friendly competition, for the HPWC category (hybrid systems with piecewice constant dynamics). In this page we repeat the corresponding experimental evaluation, using PHAVerLite version 0.2. The corresponding model and configuration files can be downloaded. People interested in details about some of the techniques used in PHAVerLite are referred to the following paper:

Anna Becchi and Enea Zaffanella
Revisiting Polyhedral Analysis for Hybrid Systems
Static Analysis - 26th International Symposium (SAS 2019) (Porto, Portugal, October 2019)

The HPWC category of the ARCH-COMP 2019 friendly competition featured 25 tests. These are divided into 15 safe tests (aiming at proving a valid safety property, so that an overapproximation of the reachable set is permitted) and 10 unsafe tests (aiming at disproving an invalid safety property, so that no overapproximation of the reachable set is permitted).

The following observations apply:

• the one reported is the total time of the analysis tool: besides the time spent in the fixpoint computation of the reachable set, it includes the parsing of the automaton (quite often also requiring the computation of the parallel composition of several automata components), as well as the computation and output of the final result;
• the timeout threshold for PHAVerLite was set to 10 minutes (PHAVer/SX and PHAVer-lite/SX were using a higher timeout threshold);
• the time reported for PHAVer/SX and PHAVer-lite/SX are taken from the ARCH-COMP 2018 edition, where 20 tests were considered; the entry n/a means not available, i.e., no attempt was performed on that test;
• PHAVer/SX was using a different machine, with a faster CPU.

The following is the table for the 15 safe tests. Note that, in all but the TTE tests, PHAVerLite overapproximates the reachable set by using a single polyhedron per location, also further approximating the convex polyhedral hull using the constraint hull (PHAVer/SX and PHAVerLite/SX perform no overapproximation).

The following is the table for the 10 unsafe tests. In this case no overapproximation is allowed, hence all tools compute on a domain of finite sets of NNC polyhedra (no use of convex polyhedral hull, constraint hull or widening operators). However, PHAVerLite checks for a violation of the safety property during the fixpoint computation, stopping as soon as possible; in contrast, PHAVer/SX and PHAVer-lite/SX compute the full reachable set and check for violation only at the end (this also explains why these tools obtain the same time on all of the variants of the DRNW02 test).