---

Abstract

Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been proposed. We contribute a replicable and thorough comparative evaluation of the state of the art: We (1) implemented a standalone PDR algorithm and, as improvement, a PDR-based auxiliary-invariant generator for k‑induction, and (2) performed an experimental study on the largest publicly available benchmark set of C verification tasks, in which we explore the effectiveness and efficiency of software verification with PDR. The main contribution of our work is to establish a reproducible baseline for ongoing research in the area by providing a well-engineered reference implementation and an experimental evaluation of the existing techniques.

---

Content

The supplementary archive contains CPAchecker and all data from our experiments. The following files are in this archive:

• CPAchecker in revision 27 742 from the trunk
• The additional test-set definitions used for the experiments
• The newly created tasks used for our experiments (the pre-existing set of tasks is available via GitHub)
• The results presented in our paper
• A README file explaining how to reproduce the results

---

Results

The result tables of the figures in our article are also available:

• Table for SVCOMP tasks for both CTIGAR implementations, for k‑induction without auxiliary invariants, and for the best configurations of each tool: k‑induction with continuously-refined data-flow and KIPDR invariants, SeaHorn, and Vvt as a portfolio verifier (Table 2 from the article)
• Table for SVCOMP tasks not solved by plain k‑induction without auxiliary invariants for different k‑induction configurations with auxiliary-invariant generation approaches (Table 3 from the article)
• Table for path programs not solved by plain k‑induction without auxiliary invariants for different k‑induction configurations with auxiliary-invariant generation approaches (Table 4 from the article)
• Table for SVCOMP tasks not solved by plain k‑induction without auxiliary invariants but solved by k‑induction with KIPDR-based auxiliary-invariant generation for different template-based data-flow invariant-generation approaches (Table 5 from the article)
• Table for hand-crafted tasks for different template-based invariant-generation approaches compared to KIPDR-based invariant generation (Table 6 from the article)
• Table from SV-COMP 2019, the last seven result rows of which show the results of the SV-COMP competitors on our seven hand-crafted tasks, which Table 7 from our article compares against k‑induction with KIPDR-based auxiliary-invariant generation (KIKIPDR).
• Table for tasks from the SV-COMP 2019 category on loops for the three best tools from SV‑COMP 2019, as well as for k‑induction with KIPDR-based auxiliary-invariant generation and for k‑induction with continuously-refined data-flow and KIPDR invariants (Table 8 from the article)

You can click on the cells in the status columns of the different algorithms in these tables to see their log output.