The Lattice-Theoretic Essence of Property Directed Reachability Analysis

TL;DR

This paper introduces LT-PDR, a lattice-theoretic generalization of the PDR algorithm, revealing its core principles and providing concrete instances, implementations, and experimental evaluations.

Contribution

It presents a novel lattice-theoretic framework for PDR, including multiple concrete instances, a generic implementation, and a categorical structural theory.

Findings

Four concrete instances of LT-PDR derived and implemented.

Experimental evaluation demonstrates effectiveness of the instances.

Categorical theory provides structural insights into LT-PDR.

Abstract

We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster-Tarski and Kleene theorems. We introduce four concrete instances of LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances.