Towards Practical Predicate Analysis
Comparison of SMT Solvers and Theories
Reproducibility of Results
Here everything is provided to reproduce the results from Chapter 16:
- CPAchecker revision 24567 (project webpage, browse source)
- BenchExec benchmark definitions
(The *-solver-theories.xml files contain the definitions for the benchmarks of Sections 16.1 and 16.3, the *-solver-sound-overflows.xml files contain the definitions for the benchmarks of Sections 16.2.) - Verification tasks from SV-Benchmarks repository (git tag svcomp17)
- BenchExec
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)
| MathSAT5 | Princess | SMTInterpol | Z3 | |
|---|---|---|---|---|
| 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)
| MathSAT5 | Princess | SMTInterpol | Z3 | |
|---|---|---|---|---|
| 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)
| MathSAT5 | Princess | SMTInterpol | Z3 | |
|---|---|---|---|---|
| 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:
- Verifiers from SV-COMP'17 (as in upper part of Table 17.1)
- Configurations of Predicate CPA with MathSAT5 and QF_UFBVFP (as in lower part of Table 17.1)
- Combination: Subset of verifiers from SV-COMP'17 and configurations of Predicate CPA (as in Figure 17.1)
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”.