一句话：提出状态与谓词间的归纳对偶性，并据此构造首个真正原始-对偶的不变式推断算法，可验证分布式协议。
不变式推断常同时涉及状态与谓词两类推理，二者被认为存在对偶关系，但缺乏形式化刻画与算法化利用。本文提出新的“归纳对偶”：基于增量归纳的可证明性概念与可达性形式对偶，且对偶结构高度对称。由此可推出经典 Houdini 算法的对偶算法，并将 Houdini 与其对偶结合，得到 primal-dual Houdini——首个真正原始-对偶的不变式推断算法。作者实现早期原型并用于分布式协议验证，能够处理文献中的困难基准。
Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use it to derive a new primal-dual invariant inference algorithm. The new induction duality is based on a notion of provability by incremental induction that is formally dual to reachability, and the duality is surprisingly symmetric. The symmetry allows us to derive the dual of the well-known Houdini algorithm, and by combining Houdini with its dual image we obtain primal-dual Houdini , the first truly primal-dual invariant inference algorithm. An early prototype of primal-dual Houdini for the domain of distributed protocol verification can handle difficult benchmarks from the literature.
@article{paperbot1538,
title = {Induction duality: primal-dual search for invariants},
author = {Oded Padon and James R. Wilcox and Jason R. Koenig and Kenneth L. McMillan and Alex Aiken},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498712}
}