The Lattice-Theoretic Essence of?Property Directed Reachability Analysis
The Lattice-Theoretic Essence of?Property Directed Reachability Analysis
复制标题
属性导向可达性分析的格理论本质
DOI：
10.1007/978-3-031-13185-1_12
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Hasuo Ichiro
中科院分区：
文献类型：
--
作者：
Kori Mayuko;Urabe Natsuki;Katsumata Shin-ya;Suenaga Kohei;Hasuo Ichiro
我们提出了LT-PDR，布拉德利的属性定向可达性分析（PDR）算法的格论推广。LT-PDR将PDR的本质确定为基于Knaster-Tarski和Kleene定理的验证和反驳尝试的巧妙组合。我们介绍了四个具体的LT-PDR的实例，从一个通用的Haskell实现LT-PDR的实现，并进行实验评估。我们还提出了一个分类结构理论，得出这些情况。
We presentLT-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.