VMCAI 2026
Mon 12 - Tue 13 January 2026 Rennes, France
co-located with POPL 2026
Mon 12 Jan 2026 11:00 - 11:30 at Horizons - Analysis 2 Chair(s): Benoît Montagu

Sound static analysis can prove the absence of data races by establishing that no two conflicting memory accesses can occur at the same time. We repurpose the concept of digests — summaries of computational histories originally introduced to bring tunable concurrency-sensitivity to thread-modular value analysis by abstract interpretation. We extend this idea to race detection and use digests to capture the conditions under which conflicting accesses may not happen in parallel. To formalize this, we give a definition of data races in the thread-modular local trace semantics and show how exclusion criteria for potential conflicts can be expressed as digests. We report on our implementation of digest-driven data race detection in the static analyzer Goblint, and evaluate it on the Sv-Comp benchmark suite. Combining the lockset digest with digests reasoning on thread ids and thread joins increases the number of correctly solved tasks by more than a factor of five compared to lockset reasoning alone.

Mon 12 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

11:00 - 12:30
Analysis 2VMCAI 2026 at Horizons
Chair(s): Benoît Montagu Inria
11:00
30m
Talk
Data Race Detection by Digest-Driven Abstract Interpretation
VMCAI 2026
Michael Schwarz National University of Singapore, Julian Erhard TU Munich; LMU Munich
Pre-print
11:30
30m
Talk
Termination Resilience Static Analysis
VMCAI 2026
Naïm Moussaoui Remil Inria & ENS | PSL, Paris, France, Caterina Urban Inria Paris - ENS - Université PSL
12:00
30m
Talk
Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification
VMCAI 2026
Andreas Lindner Uppsala universitet, Karl Palmskog KTH Royal Institute of Technology, Scott Constable Intel Corporation, Mads Dam KTH, Roberto Guanciale KTH Royal Institute of Technology, Hamed Nemati KTH Royal Institute of Technology