Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Property Directed Reachability with Extended Resolution

Andrew Luka, Yakir Vizel

TL;DR

This work introduces PdrER, a model-checking algorithm that extends Property Directed Reachability (Pdr) by employing Extended Resolution ($ER$) to construct shorter proofs of correctness. To manage the challenges of $ER$ in the model-checking setting, the authors implement template-guided extension, a delta-trace re-encoding strategy, and program-specific adjustments such as GeneralizeER, PropagateER, and ImplicationER to handle auxiliary variables. Experimental evaluation on the Hardware Model Checking Competition benchmarks demonstrates that PdrER solves more instances and often with shorter proofs and faster runtimes than Pdr and ABC’s Pdr, including problems that Pdr cannot solve within time limits. The results indicate that strong proof systems like $ER$ can be made practically usable in model checking, suggesting a significant step toward integrating powerful logical frameworks into verification tools.

Abstract

Property Directed Reachability (\textsc{Pdr}), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While \textsc{Pdr} is effective in finding inductive invariants, its underlying proof system, Resolution, limits its ability to construct short proofs for certain verification problems. This paper introduces \textsc{PdrER}, a novel generalization of \textsc{Pdr} that uses Extended Resolution (ER), a proof system exponentially stronger than Resolution, when constructing a proof of correctness. \PdrEV leverages ER to construct shorter bounded proofs of correctness, enabling it to discover more compact inductive invariants. While \PdrEV is based on \textsc{Pdr}, it includes algorithmic enhancements that had to be made in order to efficiently use ER in the context of model checking. We implemented \textsc{PdrER} in a new open-source verification framework and evaluated it on the Hardware Model Checking Competition benchmarks from 2019, 2020 and 2024. Our experimental evaluation demonstrates that \textsc{PdrER} outperforms \textsc{Pdr}, solving more instances in less time and uniquely solving problems that \textsc{Pdr} cannot solve within a given time limit. We argue that this paper represents a significant step toward making strong proof systems practically usable in model checking.

Property Directed Reachability with Extended Resolution

TL;DR

This work introduces PdrER, a model-checking algorithm that extends Property Directed Reachability (Pdr) by employing Extended Resolution () to construct shorter proofs of correctness. To manage the challenges of in the model-checking setting, the authors implement template-guided extension, a delta-trace re-encoding strategy, and program-specific adjustments such as GeneralizeER, PropagateER, and ImplicationER to handle auxiliary variables. Experimental evaluation on the Hardware Model Checking Competition benchmarks demonstrates that PdrER solves more instances and often with shorter proofs and faster runtimes than Pdr and ABC’s Pdr, including problems that Pdr cannot solve within time limits. The results indicate that strong proof systems like can be made practically usable in model checking, suggesting a significant step toward integrating powerful logical frameworks into verification tools.

Abstract

Property Directed Reachability (\textsc{Pdr}), also known as IC3, is a state-of-the-art model checking algorithm widely used for verifying safety properties. While \textsc{Pdr} is effective in finding inductive invariants, its underlying proof system, Resolution, limits its ability to construct short proofs for certain verification problems. This paper introduces \textsc{PdrER}, a novel generalization of \textsc{Pdr} that uses Extended Resolution (ER), a proof system exponentially stronger than Resolution, when constructing a proof of correctness. \PdrEV leverages ER to construct shorter bounded proofs of correctness, enabling it to discover more compact inductive invariants. While \PdrEV is based on \textsc{Pdr}, it includes algorithmic enhancements that had to be made in order to efficiently use ER in the context of model checking. We implemented \textsc{PdrER} in a new open-source verification framework and evaluated it on the Hardware Model Checking Competition benchmarks from 2019, 2020 and 2024. Our experimental evaluation demonstrates that \textsc{PdrER} outperforms \textsc{Pdr}, solving more instances in less time and uniquely solving problems that \textsc{Pdr} cannot solve within a given time limit. We argue that this paper represents a significant step toward making strong proof systems practically usable in model checking.

Paper Structure

This paper contains 27 sections, 6 theorems, 8 equations, 8 figures, 1 table, 6 algorithms.

Table of Contents

  1. Introduction
  2. Related Work
  3. Preliminaries
  4. Safety verification:
  5. Relative induction:
  6. Property Directed Reachability
  7. Redundancy:
  8. Propagation:
  9. Generalization:
  10. Applying the Extension Rule
  11. Matching Templates on an Inductive Trace
  12. Multiple CNFs:
  13. Evolving CNF:
  14. Matching Algorithm:
  15. PdrER
  16. ...and 12 more sections

Key Result

lemma 1

If a transition system $T$ admits a safe trace $\vec{F}$ of size $|\vec{F}| = N$, then $T$ does not admit counterexamples of length less than, or equal to $N$.

Figures (8)

  • Figure 1: Clauses at the top match $\tau_{\land}$, $\tau_{\oplus}$ and $\tau_{ha}$ from left to right, respectively. Applying the extension rule transform them into the clauses at the bottom. The instantiations are $\{\{a\},\{b\}\}$ for $\tau_{\land}$, $\{\{ a,b\},\{\neg a, \neg b\}\}$ for $\tau_{\oplus}$ and $\{\{ a, b, c\}, \{ a, b, d\}, \{ \neg a, \neg b,c,d \} \}$ for $\tau_{ha}$.
  • Figure 2: HWMCC results, average runtime is in seconds
  • Figure 3: HWMCC'19/20/24
  • Figure 4: Auxiliary Variables (AVs) added and used by PdrER. %$\oplus$ stand for percentage of AVs using $\oplus$ in their definition.
  • Figure 5: Proof comparison: PdrER vs. Pdr. X-axis is Pdr across all plots. (\ref{['fig:invar_2024']})-(\ref{['fig:po_24']}) HWMCC'24, (\ref{['fig:invar_19_20']})-(\ref{['fig:po_19_20']}) HWMCC'19/20.
  • ...and 3 more figures

Theorems & Definitions (15)

  • lemma 1
  • theorem 1
  • definition 1: Match
  • definition 2: Instantiation
  • definition 3: Auxiliary Circuit
  • definition 4: Generalized Invariant
  • lemma 2
  • proof
  • lemma 3: Auxiliary Variable Elimination
  • proof : Sketch
  • ...and 5 more