Simmo Saan

Computer science PhD student specializing in static program analysis and programming languages at University of Tartu in Estonia.

Currently the lead developer and maintainer of Goblint, a static analysis framework for C. Also a contributor to the OCaml ecosystem at large.

Prolific (functional) programmer and open source aficionado in general: sim642 on GitHub.

news

Oct 25, 2023	📄 Published preprint Correctness Witness Validation by Abstract Interpretation.
Jun 6, 2023	📄 Published When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-Local Jumps in C.
Apr 20, 2023	📄 Published Goblint: Autotuning Thread-Modular Abstract Interpretation (Competition Contribution).
Apr 17, 2023	📄 Published Clustered Relational Thread-Modular Abstract Interpretation with Local Traces.
Feb 4, 2023	🏆 Goblint won the data race category in SV-COMP 2023 (results).

selected publications

2023

arXiv

Correctness Witness Validation by Abstract Interpretation

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

2023

To appear in Verification, Model Checking, and Abstract Interpretation

Abs arXiv Supp

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.