Software model-checking as cyclic-proof search
Software model-checking as cyclic-proof search
复制标题
DOI：
10.1145/3498725
复制
发表时间：
2021-11
影响因子：
--
通讯作者：
Takeshi Tsukada;Hiroshi Unno
中科院分区：
文献类型：
--
作者：
Takeshi Tsukada;Hiroshi Unno
本文表明，各种软件模型检查算法可以被视为非标准证明系统（称为循环证明系统）的证明搜索策略。我们使用循环证明系统作为软件模型检查的逻辑基础，使我们能够比较不同的算法，从几个简单的原理重构众所周知的算法，并免费获得算法的健全性证明。除其他外，我们展示了基于我们称为最大保守性的概念的启发式的重要性；这解释了诸如属性导向可达性（PDR）之类的重要算法的核心，并揭示了与无限图博弈的高效求解器之间的令人惊讶的联系，而该求解器不被视为一种 PDR。
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our use of the cyclic proof system as a logical foundation of software model checking enables us to compare different algorithms, to reconstruct well-known algorithms from a few simple principles, and to obtain soundness proofs of algorithms for free. Among others, we show the significance of a heuristics based on a notion that we call maximal conservativity; this explains the cores of important algorithms such as property-directed reachability (PDR) and reveals a surprising connection to an efficient solver of games over infinite graphs that was not regarded as a kind of PDR.