Software Verification with PDR:
Implementation and Empirical Evaluation of the State of the Art

Dirk Beyer and Matthias Dangl


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.


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


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

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