论文标题
财产的晶格理论本质定向可及性分析
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
论文作者
论文摘要
我们提出了LT-PDR，这是Bradley属性的晶格理论概括（PDR）算法。 LT-PDR将PDR的本质鉴定为基于担验证和反驳尝试的巧妙组合。我们介绍了LT-PDR的四个具体实例，从LT-PDR的通用Haskell实施中得出了实施，并对它们进行了评估。我们还提出了一种推导这些实例的分类结构理论。
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.
