Towards Practical Predicate Analysis

— Supplementary Web Page —
Thesis

Philipp Wendler

Comparison of SMT Solvers and Theories

Reproducibility of Results

Here everything is provided to reproduce the results from Chapter 16:

Full Results

The raw results are available in the format of BenchExec, which can be processed with table-generator, for example for creating interactive tables or CSV files. We also provide tables with the full results. Because of their size, the results are split into tables for each combination of verification algorithm and SMT solver.

Results for Bitprecise Theories (Section 16.1)

MathSAT5PrincessSMTInterpolZ3
BMC results / table results / table
k-Induction results / table results / table
Impact results / table results / table
Predicate Abstraction results / table results / table

Results for Theories with Linear Arithmetic (Section 16.2)

MathSAT5PrincessSMTInterpolZ3
BMC results / table results / table results / table results / table
k-Induction results / table results / table results / table results / table
Impact results / table results / table results / table results / table
Predicate Abstraction results / table results / table results / table results / table

Results for Theories with Linear Arithmetic with Unsound Encoding (Section 16.3)

MathSAT5PrincessSMTInterpolZ3
BMC results / table results / table results / table results / table
k-Induction results / table results / table results / table results / table
Impact results / table results / table results / table results / table
Predicate Abstraction results / table results / table results / table results / table

Note that all these result files do not contain data for the four verification tasks psyco_cev_1_false-unreach-call.c, psyco_cev_2_false-unreach-call.c, psyco_cev_3_false-unreach-call.c, and psyco_net_1_false-unreach-call.c from the category ECA (thus, there are only 5590 instead of 5594 verification tasks in these tables). These four tasks lead to a crash of CPAchecker's frontend because of their complexity. In order to not confuse this error that is not related to our predicate analysis with other errors, these four tasks are not present in the tables.

Comparison with State of the Art

The results for configurations of the Predicate CPA in Chapter 17 are a subset of the results from Chapter 16 that are provided above.

The results for verifiers from SV-COMP'17 are the official results of SV-COMP'17 (raw results). Note that in our comparison only a subset of the SV-COMP'17 categories and no witness validation was used, and thus the summary data differs from SV-COMP'17. Archives with the verifiers from SV-COMP'17 can be download from the SV-COMP'17 webpage.

Tables with full results:

Impact of Hardware Characteristics on Parallel Tool Executions

The data for the benchmarks from Chapter 11 (Impact of Hardware Characteristics on Parallel Tool Executions) can be found on the supplementary webpage four our paper “Reliable Benchmarking: Requirements and Solutions”.