publications

2025

1. VMCAI

   Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts

   Julian Erhard, Manuel Bentele, Matthias Heizmann, and 7 more authors

   In Verification, Model Checking, and Abstract Interpretation, 2025

   To appear

   Abs arXiv Supp

   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.

2024

1. arXiv

   Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)

   Julian Erhard, Manuel Bentele, Matthias Heizmann, and 7 more authors

   2024

   To appear in Verification, Model Checking, and Abstract Interpretation

   Abs arXiv Supp

   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.

2. Onward!

   Abstract Debuggers: Exploring Program Behaviors using Static Analysis Results

   Karoliine Holter, Juhan Oskar Hennoste, Patrick Lam, and 2 more authors

   In New Ideas, New Paradigms, and Reflections on Programming and Software, 2024

   Abs DOI Video Code

   Traditional, or concrete, debuggers allow developers to step through programs and explore the corresponding concrete program states—developers can query current values of program variables. This exploration enables developers to formulate and refine hypotheses about program behaviors. We propose the novel notion of abstract debuggers, which allow developers to explore abstract program states, as computed by sound static analyzers. Giving developers the ability to interactively explore abstract states empowers them to work with hypotheses that are true for all program executions: they can examine and rule out false positives, or better understand a static analysis’s declaration that some code is indeed safe. Abstract debuggers’ interfaces, reminiscent of conventional debuggers, aim to make navigating and interpreting static analysis results more straightforward. We have formalized the concept, applied it by implementing a tool that leverages the static analyzer Goblint, and illustrate its usefulness through case studies.

3. STTT

   Interactive abstract interpretation: reanalyzing multithreaded C programs for cheap

   Julian Erhard, Simmo Saan, Sarah Tilscher, and 4 more authors

   Software Tools for Technology Transfer, 2024

   Abs DOI arXiv Supp Code

   To put sound program analysis at the fingertips of the software developer, we propose a framework for interactive abstract interpretation of multithreaded C code. Abstract interpretation provides sound analysis results, but can be quite costly in general. To achieve quick response times, we incrementalize the analysis infrastructure, including postprocessing, without necessitating any modifications to the analysis specifications themselves. We rely on the local generic fixpoint engine TD – which we enhance with reluctant destabilization to minimize reanalysis effort. Dedicated further improvements support precise incremental analysis of program properties that include concurrency deficiencies such as data-races. The framework has been implemented in the static analyzer Goblint, and combined with the MagpieBridge framework to relay findings to IDEs. We evaluate our implementation w.r.t. the yard sticks of response time and consistency. We also provide examples of program development highlighting the usability of our approach.

4. DEBT

   Abstract Debugging with GobPie

   Karoliine Holter, Juhan Oskar Hennoste, Simmo Saan, and 2 more authors

   In Future Debugging Techniques, 2024

   Abs DOI Video Code

   GobPie is an IDE integration designed to enhance the usability and explainability of the abstract interpretation-based static analyzer Goblint. GobPie features abstract debugging, a novel approach to presenting static analysis results, which complements traditional debugging methods by making program analysis results visible. Its goal is to help resolve rare but real software issues. Unlike traditional debugging, which proceeds step-by-step to observe concrete states, abstract debugging uses static analysis results to simulate the same steps, offering insights into all possible execution paths.

5. STTT

   When long jumps fall short: control-flow tracking and misuse detection for nonlocal jumps in C: Extended version

   Michael Schwarz, Julian Erhard, Vesal Vojdani, and 2 more authors

   Software Tools for Technology Transfer, 2024

   Abs DOI Supp Code

   The C programming language offers setjmp/longjmp as a mechanism for nonlocal control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies – leading to subtle programming errors. At the same time, most static analyzers lack proper support, implying that otherwise sound tools miss whole classes of program deficiencies. We propose a concrete semantics of a subset of C with setjmp/longjmp, where interprocedural longjmps are performed directly, as well as an equivalent formulation where such jumps are implemented via stack-unwinding at the call-sites. Reflecting this semantic equivalence, we propose an approach for lifting existing interprocedural analyses to support setjmp/longjmp and to flag their misuse. To deal with the nonlocal semantics, our approach leverages side-effecting transfer functions, which, when executed, may additionally trigger contributions for program points that are not static control-flow successors. We showcase our analysis on a real-world example and propose a set of litmus tests for other analyzers.

6. TACAS

   Goblint Validator: Correctness Witness Validation by Abstract Interpretation (Competition Contribution)

   Simmo Saan, Julian Erhard, Michael Schwarz, and 5 more authors

   In Tools and Algorithms for the Construction and Analysis of Systems, 2024

   Abs DOI Supp Code Slides

   Goblint is an abstract interpretation framework for C programs with a specialty in concurrency. Using a novel approach, we turn it into a validator of YAML correctness witnesses for all SV-COMP categories. We describe its results at SV-COMP 2024 which includes the first large-scale evaluation of our validator.

7. TACAS

   Goblint: Abstract Interpretation for Memory Safety and Termination (Competition Contribution)

   Simmo Saan, Julian Erhard, Michael Schwarz, and 5 more authors

   In Tools and Algorithms for the Construction and Analysis of Systems, 2024

   Abs DOI Supp Code Slides

   Goblint is an abstract interpreter of C programs, focusing on the analysis of multi-threaded code. It is equipped with a variety of abstract domains, as well as analyses which allow it to reason about an array of program properties in a highly configurable manner. Goblint has been extended with support for the detection of memory safety bugs and non-termination.

8. VMCAI

   Correctness Witness Validation by Abstract Interpretation

   Simmo Saan, Michael Schwarz, Julian Erhard, and 3 more authors

   In Verification, Model Checking, and Abstract Interpretation, 2024

   🥇 Best Paper Award Abs DOI arXiv Supp Video Code

   https://popl24.sigplan.org/home/VMCAI-2024#Best-Paper-Award

   Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.

2023

1. SOAP

   When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-Local Jumps in C

   Michael Schwarz, Julian Erhard, Vesal Vojdani, and 2 more authors

   In State Of the Art in Program Analysis, 2023

   Abs DOI Supp Code

   The C programming language offers setjmp/longjmp as a mechanism for non-local control flow. This mechanism has complicated semantics. As most developers do not encounter it day-to-day, they may be unfamiliar with all its intricacies – leading to subtle programming errors. At the same time, most static analyzers lack proper support, implying that otherwise sound tools miss whole classes of program deficiencies. We propose an approach for lifting existing interprocedural analyses to support setjmp/longjmp, as well as to flag their misuse. To deal with the non-local semantics, our approach leverages side-effecting transfer functions which, when executed, may trigger contributions to extra program points. We showcase our analysis on real-world examples and propose a set of litmus tests for other analyzers.

2. TACAS

   Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution)

   Simmo Saan, Michael Schwarz, Julian Erhard, and 4 more authors

   In Tools and Algorithms for the Construction and Analysis of Systems, 2023

   Abs DOI Supp Code Slides

   The static analyzer Goblint is dedicated to the analysis of multi-threaded C programs by abstract interpretation. It provides multiple techniques for increasing analysis precision, e.g., configurable context-sensitivity and a wide range of numerical analyses. As a rule of thumb, more precise analyses decrease scalability, while not always necessary for solving the task at hand. Therefore, Goblint has been enhanced with autotuning which, based on syntactical criteria, adapts analysis configuration to the given program such that relevant precision is obtained with acceptable effort.

3. ESOP

   Clustered Relational Thread-Modular Abstract Interpretation with Local Traces

   Michael Schwarz, Simmo Saan, Helmut Seidl, and 2 more authors

   In European Symposium on Programming, 2023

   Abs DOI arXiv Supp Code

   We construct novel thread-modular analyses that track relational information for potentially overlapping clusters of global variables – given that they are protected by common mutexes. We provide a framework to systematically increase the precision of clustered relational analyses by splitting control locations based on abstractions of local traces. As one instance, we obtain an analysis of dynamic thread creation and joining. Interestingly, tracking less relational information for globals may result in higher precision. We consider the class of 2-decomposable domains that encompasses many weakly relational domains (e.g., Octagons). For these domains, we prove that maximal precision is attained already for clusters of globals of sizes at most 2.

2021

1. SAS

   Improving Thread-Modular Abstract Interpretation

   Michael Schwarz, Simmo Saan, Helmut Seidl, and 3 more authors

   In Static Analysis Symposium, 2021

   Abs DOI arXiv Supp Video Code

   We give thread-modular non-relational value analyses as abstractions of a local trace semantics. The semantics as well as the analyses are formulated by means of global invariants and side-effecting constraint systems. We show that a generalization of the analysis provided by the static analyzer Goblint as well as a natural improvement of Antoine Miné’s approach can be obtained as instances of this general scheme. We show that these two analyses are incomparable w.r.t. precision and provide a refinement which improves on both precision-wise. We also report on a preliminary experimental comparison of the given analyses on a meaningful suite of benchmarks.

2. TACAS

   Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints (Competition Contribution)

   Simmo Saan, Michael Schwarz, Kalmer Apinis, and 4 more authors

   In Tools and Algorithms for the Construction and Analysis of Systems, 2021

   Abs DOI Supp Video Code Slides

   Goblint is a static analysis framework for C programs specializing in data race analysis. It relies on thread-modular abstract interpretation where thread interferences are accounted for by means of flow-insensitive global invariants.

2019

1. NWPT

   Approaches to Thread-Modular Static Analysis

   Vesal Vojdani, Kalmer Apinis, and Simmo Saan

   In Nordic Workshop on Programming Theory (Abstracts), 2019

   PDF

2020

1. MSc

   Witness Generation for Data-flow Analysis

   Simmo Saan

   University of Tartu, 2020

   Supervisor: Vesal Vojdani

   Abs HTML PDF Code Slides

   A program analyzer, which determines whether a given program satisfies or violates the specification, may itself contain bugs and thus be untrustworthy. Hence, the analyzer should back its claims with witnesses, which can be understood by the programmer and automatically checked by independent tools. Interprocedural data-flow analysis is well-suited for certain problems but its abstractions do not directly correspond to required witnesses. We show that witnesses can be generated with data-flow analysis by designing the necessary methods to handle interprocedurality and adapting a technique from model checking to increase precision of the generated witnesses. The ideas are implemented and experimentally evaluated in the data-flow analyzer Goblint. This allows improving trustworthiness and usability of data-flow analyzers and enables their comparison with other verifiers.

2018

1. BSc

   Property-based Testing of Abstract Domains 🇪🇪

   Simmo Saan

   University of Tartu, 2018

   Supervisors: Vesal Vojdani, Kalmer Apinis

   Abs HTML PDF Code Slides

   Static program analysis studies programs based on their source code, without executing them. One approach is to use abstract interpretation to determine a program’s possible approximate states, which make up an abstract domain. If the used domain satisfies certain mathematical properties, then the analysis is sound according to the theory of abstract interpretation. When implementing a static analyzer it may happen that the domains contain bugs, which ruin the analysis and its soundness. Here a set of properties is compiled, which are used to find bugs from the Goblint analyzer via property-based testing. For this the necessary domain testing framework and element generators are implemented in Goblint. Finally the testing is conducted, issues identified and described. This shows that property-based testing can effectively be used to find bugs from abstract domains.