  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.
