The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Logic in Computer Science
2022-08-16 v4 Programming Languages
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.
Keywords
Cite
@article{arxiv.2203.14261,
title = {The Lattice-Theoretic Essence of Property Directed Reachability Analysis},
author = {Mayuko Kori and Natsuki Urabe and Shin-ya Katsumata and Kohei Suenaga and Ichiro Hasuo},
journal= {arXiv preprint arXiv:2203.14261},
year = {2022}
}
Comments
37 pages