Incremental Property Directed Reachability

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 instances, progressively increasing the allowed number of interleavings. The experimental results demonstrate significant performance improvements compared to Z3's PDR implementation SPACER. Experiments also show that the incremental approach succeeds in reusing a substantial amount of clauses between instances, for both the constraining and relaxing algorithm.