Parameterized verification is a challenging problem that is known to be undecidable in the general case. CMP 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 CMP 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 CMP 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 CMP, 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 CMP to the FLASH cache coherence protocol.
Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change
13:40 - 15:20 | Program Synthesis and Verification 1OOPSLA 2024 at IBR West Chair(s): Benjamin Delaware Purdue University | ||
13:40 20mTalk | Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis OOPSLA 2024 Benjamin Mariano University of Texas at Austin, Ziteng Wang University of Texas at Austin, Shankara Pailoor University of Texas at Austin, Christian Collberg University of Arizona, Işıl Dillig University of Texas at Austin DOI | ||
14:00 20mTalk | Finding ∀∃ Hyperbugs Using Symbolic Execution OOPSLA 2024 Arthur Correnson CISPA Helmholtz Center for Information Security, Tobias Nießen TU Wien, Bernd Finkbeiner CISPA Helmholtz Center for Information Security, Georg Weissenbacher TU Wien DOI | ||
14:20 20mTalk | Mechanizing the CMP Abstraction for Parameterized Verification OOPSLA 2024 Yongjian Li Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China, Bohua Zhan Institute of Software, Chinese Academy of Sciences, Jun Pang University of Luxembourg DOI | ||
14:40 20mTalk | Model Checking Distributed Protocols in Must OOPSLA 2024 Constantin Enea LIX, CNRS, Ecole Polytechnique, Dimitra Giannakopoulou Amazon Web Services, Michalis Kokologiannakis ETH Zurich, Rupak Majumdar MPI-SWS DOI | ||
15:00 20mTalk | Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials OOPSLA 2024 DOI |