Thu 24 Oct 2024 14:20 - 14:40 at IBR West - Program Synthesis and Verification 1 Chair(s): Benjamin Delaware

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 Oct

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
OOPSLA 2024
Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University
DOI