Back to Search
Start Over
Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art
- Publication Year :
- 2019
-
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.<br />Comment: 35 pages, 8 tables, 13 figures, supplementary web page: https://www.sosy-lab.org/research/pdr-compare/, replication package: https://doi.org/10.5281/zenodo.3370037
- Subjects :
- Computer Science - Software Engineering
Subjects
Details
- Database :
- arXiv
- Publication Type :
- Report
- Accession number :
- edsarx.1908.06271
- Document Type :
- Working Paper