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 17:00 - 17:30 at Hopscotch - Concurrency

Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists — in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75 % of these witnesses — indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.

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, 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