Title: Thread-Modular Abstract Interpretation with Goblint

Abstract: Concurrent programs are notoriously hard to analyze because of the combinatorial explosion faced when considering all possible interleavings. Thread-modular abstract interpretation mitigates this by analyzing each thread in isolation as much as possible while coarsely approximating interactions between threads. In this tutorial, we present thread-modular analyses derived as abstract interpretations of the local trace semantics, a thread-modular concrete semantics focusing on the local perspectives of threads. We then show how digests, i.e., computational history abstractions, can be used to exclude spurious thread interactions and improve analysis precision. Finally, we present a unifying formalism for implementing different approaches to thread-modular analysis within a single tool, and introduce the Goblint static analysis framework, which supports rapid prototyping of new thread-modular analyses.