一句话：将多种软件模型检测算法统一为循环证明系统中的证明搜索策略，并揭示极大保守性启发式的意义。
本文研究软件模型检测算法之间的逻辑基础与统一理解问题。作者提出将这些算法视为非标准证明系统——循环证明系统——中的证明搜索策略，从而比较不同算法、从少数简单原则重构已知算法，并免费获得可靠性证明。论文特别强调一种称为“极大保守性”的启发式，说明 property-directed reachability（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.