Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
ACM SIGPLAN via YouTube
Overview
Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
This conference talk presents a new framework for verifying systems with a parametric number of concurrent processes. Learn about well-structured systems and how they enable decision-making for verification problems like control-state reachability, coverability, and target through a fixed finite abstraction called a 01-counter system. The speakers, Paul Eichler, Swen Jacobs, and Chana Weil-Kennedy from CISPA and IMDEA Software Institute, demonstrate how various systems from parameterized verification literature—including reconfigurable broadcast networks, disjunctive systems, synchronizations, and systems with shared finite-domain variables—fit into this unified framework. Discover how this approach provides simpler explanations for previously separately-investigated system properties while extending existing results and identifying new systems with similar characteristics. The talk was presented at the VMCAI conference in January 2025, sponsored by ACM SIGPLAN.
Syllabus
[VMCAI'25] Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
Taught by
ACM SIGPLAN