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

Dirk Beyer, 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 mod…