VMCAI 2025
Mon 20 - Tue 21 January 2025 Denver, Colorado, United States
co-located with POPL 2025

This program is tentative and subject to change.

Mon 20 Jan 2025 14:30 - 15:00 at Hopscotch - Model Checking

We introduce a new framework for verifying systems with a parametric number of concurrently running processes. The systems we consider are well-structured with respect to a specific well-quasi order. This allows us to decide a wide range of verification problems, including control-state reachability, coverability, and target, in a fixed finite abstraction of the infinite state-space, called a 01-counter system. We show that several systems from the parameterized verification literature fall into this class, including reconfigurable broadcast networks (or systems with lossy broadcast), disjunctive systems, synchronizations and systems with a fixed number of shared finite-domain variables. Our framework provides a simple and unified explanation for the properties of these systems, which have so far been investigated separately. Additionally, it extends and improves on a range of the existing results, and gives rise to other systems with similar properties.

This program is tentative and subject to change.

Mon 20 Jan

Displayed time zone: Mountain Time (US & Canada) change

14:00 - 15:30
Model CheckingVMCAI 2025 at Hopscotch
14:00
30m
Talk
Space-Efficient Model-Checking of Higher-Order Recursion Schemes
VMCAI 2025
Florian Bruse University of Kassel
14:30
30m
Talk
Parameterized Verification of Systems with Precise (0,1)-Counter Abstraction
VMCAI 2025
Paul Eichler CISPA - Helmholtz Center for Information Security, Swen Jacobs CISPA, Chana Weil-Kennedy IMDEA Software Institute
15:00
30m
Talk
Property-agnostic base case extension for scalable verification of distributed systems
VMCAI 2025
Kyle Storey Brigham Young University, Eric Mercer Brigham Young University