Thread-Modular Abstract Interpretation - The Local Perspective
19/9/2025, 3:00pm
Speaker
Abstract
Multi-threaded software is notoriously hard to write, rendering static analysis techniques that scale to real-world programs while remaining sufficiently precise all the more desirable. We propose thread-modular analyses which we obtain as abstract interpretations of the local trace semantics — a new thread-modular concrete semantics focusing on the local perspectives of threads. Casting existing analyses into our framework enables a principled comparison — and spurs the development of novel, more precise analyses. For relational analyses, we once more take a local perspective and track, for each mutex, relationships within clusters of globals protected by a common mutex. To boost precision, we propose digests — computational history abstractions — to exclude spurious thread interactions. All analyses are evaluated on real-world benchmarks for runtime and precision. The talk will also touch on some of our adjacent work, such as precision-recovery for mixed flow-sensitive analyses, weakly relation domains, and witnesses for thread-modular abstract interpretation.
Bio
Michael Schwarz is a research fellow at the FOCS lab at NUS, advised by Umang Mathur. He obtained his PhD from the Technical University of Munich where he worked on Abstract Interpretation with Helmut Seidl's group. His research interests span static and dynamic techniques for program analysis as well as testing, with much of his work focused on concurrent programs. He is a key contributor to the Goblint static analyzer, which serves as the testbed for many of his ideas.