Back to Search
Start Over
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
- Publication Year :
- 2022
-
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.<br />Comment: 37 pages
Details
- Database :
- arXiv
- Publication Type :
- Report
- Accession number :
- edsarx.2203.14261
- Document Type :
- Working Paper