Incremental Property Directed Reachability
Max Blankestijn, Alfons Laarman

TL;DR
This paper introduces an incremental version of Property Directed Reachability (IPDR) that leverages incremental SAT solvers to efficiently verify systems of increasing complexity by reusing previous verification results.
Contribution
The paper presents a novel incremental PDR algorithm that supports constraining and relaxing, improving verification efficiency through clause reuse and incremental SAT solving.
Findings
Significant performance improvements over existing PDR implementations.
Effective reuse of clauses across multiple system instances.
Successful application to circuit pebbling and parallel program verification.
Abstract
Property Directed Reachability (PDR) is a widely used technique for formal verification of hardware and software systems. This paper presents an incremental version of PDR (IPDR), which enables the automatic verification of system instances of incremental complexity. The proposed algorithm leverages the concept of incremental SAT solvers to reuse verification results from previously verified system instances, thereby accelerating the verification process. The new algorithm supports both incremental constraining and relaxing; i.e., starting from an over-constrained instance that is gradually relaxed. To validate the effectiveness of the proposed algorithm, we implemented IPDR and experimentally evaluate it on two different problem domains. First, we consider a circuit pebbling problem, where the number of pebbles is both constrained and relaxed. Second, we explore parallel program…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
