VMCAI 2025
Mon 20 - Tue 21 January 2025 Denver, Colorado, United States
co-located with POPL 2025
Mon 20 Jan 2025 14:00 - 14:30 at Hopscotch - Model Checking Chair(s): Arie Gurfinkel

Model checking trees generated by order-k Higher-Order Recursion Schemes (HORS) against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong’06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT,such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is k-1-EXPSPACE-complete. The upper bound is achieved by converting the problem into an alternating reachability game, the lower one via a reduction from a tiling problem.

Mon 20 Jan

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

14:00 - 15:30
Model CheckingVMCAI 2025 at Hopscotch
Chair(s): Arie Gurfinkel University of Waterloo
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 AbstractionRemote
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
:
:
:
: