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.

Tue 21 Jan 2025 16:30 - 17:00 at Hopscotch - Concurrency

Scalable distributed systems are typically parametric in design. The key parameter is the number of isomorphic components, K. A second important parameter is the number of neighbors, k, of each component process. In this work, we describe a methodology that uses an automated synthesis procedure to construct parametric system instances where both K and k can vary arbitrarily, extending prior work on synthesis for a fixed k. The methodology relies crucially on locality, symmetry, and abstraction. The first step is to eliminate K by refining a general, system-wide specification to a local temporal specification for a generic process in its parameterized neighborhood. Next, the local process specification is abstracted to remove its dependence on k. These steps are done by hand. The given synthesis procedure then automatically constructs an abstract process from the abstract local specification with a worst-case cost exponential in the length of the abstract local specification. We show that, for any k, the concretized abstract process meets the local specification. We then show that instantiating the abstract process with different k and K forms system instances that satisfy the system-level specification. The worst-case cost of instantiation is linear in K. We use this method to synthesize an atomic snapshot protocol on fully connected networks and a dining philosophers protocol on hypercubes.

This program is tentative and subject to change.

Tue 21 Jan

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

16:00 - 17:30
ConcurrencyVMCAI 2025 at Hopscotch
16:00
30m
Talk
LLOR: Automated Repair of OpenMP Programs
VMCAI 2025
Gautam Muduganti Indian Institute of Technology Hyderabad, India, Utpal Bora University of Cambridge, Saurabh Joshi Supra Research, Ramakrishna Upadrasta
16:30
30m
Talk
Synthesis of Parametric Locally Symmetric Protocols from Abstract Temporal Specifications
VMCAI 2025
Ruoxi Zhang University of Waterloo, Richard Trefler University of Waterloo, Canada, Kedar Namjoshi Nokia Bell Labs
17:00
30m
Talk
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
VMCAI 2025
Julian Erhard LMU Munich; TU Munich, Manuel Bentele University of Freiburg, Freiburg, Germany, Matthias Heizmann University of Freiburg, Germany, Dominik Klumpp University of Freiburg, Simmo Saan University of Tartu, Estonia, Frank Schüssele University of Freiburg, Michael Schwarz TU Munich, Helmut Seidl TU Munich, Sarah Tilscher Technical University of Munich, Garching, Germany, Vesal Vojdani University of Tartu