一句话：提出反例驱动的关系抽象与细化方法，避免量词实例化导致SMT求解器发散，并验证共识协议安全性质。
形式化验证无限状态系统时，量词交替与函数符号会产生函数环，导致无穷多地项，使SMT求解器难以实例化量词甚至发散。本文提出交互式验证方法：用关系抽象将验证条件中的函数抽象为一一对应关系，避免函数环与地项增殖；该抽象可靠，若求解器找不到反模型则证明正确，但可能产生伪反例。作者通过诊断反例、手动实例化原函数值域元素来精化抽象；若VC正确，有限步精化可消除所有伪反模型，方法完备。在Ivy中验证共识协议安全性质时，多数目标可自动证明，原始VC常令SMT求解器发散；仅需少量手动实例化，反例比超时更有指导价值，且该技术可导出复杂算法的高效底层实现。
Formally verifying infinite-state systems can be a daunting task, especially when it comes to reasoning about quantifiers. In particular, quantifier alternations in conjunction with function symbols can create function cycles that result in infinitely many ground terms, making it difficult for solvers to instantiate quantifiers and causing them to diverge. This can leave users with no useful information on how to proceed. To address this issue, we propose an interactive verification methodology that uses a relational abstraction technique to mitigate solver divergence in the presence of quantifiers. This technique abstracts functions in the verification conditions (VCs) as one-to-one relations, which avoids the creation of function cycles and the resulting proliferation of ground terms. Relational abstraction is sound and guarantees correctness if the solver cannot find counter-models. However, it may also lead to false counterexamples, which can be addressed by refining the abstraction and requiring the existence of corresponding elements. In the domain of distributed protocols, we can refine the abstraction by diagnosing counterexamples and manually instantiating elements in the range of the original function. If the verification conditions are correct, there always exist finitely many refinement steps that eliminate all spurious counter-models, making the approach complete. We applied this approach in Ivy to verify the safety properties of consensus protocols and found that: (1) most verification goals can be automatically verified using relational abstraction, while SMT solvers often diverge when given the original VC, (2) only a few manual instantiations were needed, and the counterexamples provided valuable guidance for the user compared to timeouts produced by the traditional approach, and (3) the technique can be used to derive efficient low-level implementations of tricky algorithms.
@article{paperbot1897,
title = {Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols},
author = {Orr Tamir and Marcelo Taube and Kenneth L. McMillan and Sharon Shoham and Jon Howell and Guy Gueta and Mooly Sagiv},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622864}
}