Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art
This work provides a replicable baseline for ongoing research in software verification, primarily benefiting researchers in model checking, but it is incremental as it focuses on evaluation rather than new methods.
The paper tackled the problem of evaluating property-directed reachability (PDR) for software verification by implementing a standalone PDR algorithm and a PDR-based auxiliary-invariant generator for k-induction, and conducted an empirical study on a large benchmark set of C verification tasks to assess effectiveness and efficiency.
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.