一句话：在 Isabelle/HOL 中形式化验证 CMP 抽象与强化方法，并实现自动执行与生成证明脚本的工具 AutoCMP。
参数化验证在一般情况下不可判定，CMP 方法通过将协议抽象为固定小规模节点并用辅助不变式强化来应对，但已有应用多靠手工完成，理论论证也停留在高层描述。本文在 Isabelle/HOL 中给出 CMP 的形式化理论，提出语法驱动的抽象与强化过程并证明其正确性，形式化还涵盖对称约简与 assume-guarantee 推理的正确性。作者实现了工具 AutoCMP，可自动执行抽象与强化并生成对应的 Isabelle 证明脚本。该工具已应用于若干参数化协议，并在重新审视 FLASH 缓存一致性协议的先前手工应用时发现了不准确之处。
Parameterized verification is a challenging problem that is known to be undecidable in the general case. is a widely-used method for parameterized verification, originally proposed by Chou, Mannava and Park in 2004. It involves abstracting the protocol to a small fixed number of nodes, and strengthening by auxiliary invariants to refine the abstraction. In most of the existing applications of CMP, the abstraction and strengthening procedures are carried out manually, which can be tedious and error-prone. Existing theoretical justification of the method is also done at a high level, without detailed descriptions of abstraction and strengthening rules. In this paper, we present a formally verified theory of in Isabelle/HOL, with detailed, syntax-directed procedure for abstraction and strengthening that is proven correct. The formalization also includes correctness of symmetry reduction and assume-guarantee reasoning. We also describe a tool AutoCMP for automatically carrying out abstraction and strengthening in , as well as generating Isabelle proof scripts showing their correctness. We applied the tool to a number of parameterized protocols, and discovered some inaccuracies in previous manual applications of to the FLASH cache coherence protocol.
@article{paperbot2525,
title = {Mechanizing the CMP Abstraction for Parameterized Verification},
author = {Yongjian Li and Bohua Zhan and Jun Pang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649858}
}