Research Interests

• Incremental and interactive static analysis by abstract interpretation
• Verification of fixpoint algorithms in Isabelle

Projects

• Goblint - A static analyzer using abstract interpretation for analyzing multi-threaded C programs

Publications

• S. Saan, M. Schwarz, J. Erhard, H. Seidl, S. Tilscher, V. Vojdani: Correctness Witness Validation by Abstract Interpretation. VMCAI 2024: 74-97
• H. Seidl, J. Erhard, M. Schwarz, S. Tilscher: 2-Pointer Logic. Taming the Infinities of Concurrency: Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday. 2024: 281-307
• S. Saan, J. Erhard, M. Schwarz, S. Bozhilov, K. Holter, S. Tilscher, V. Vojdani, H. Seidl: Goblint: Abstract Interpretation for Memory Safety and Termination - (Competition Contribution). TACAS 2024: 381-386
• S. Saan, J. Erhard, M. Schwarz, S. Bozhilov, K. Holter, S. Tilscher, V. Vojdani, H. Seidl: Goblint Validator: Correctness Witness Validation by Abstract Interpretation - (Competition Contribution). TACAS 2024: 335-340 (paper)
• Sarah Tilscher, Yannick Stade, Michael Schwarz, Ralf Vogler, Helmut Seidl. The Top-Down Solver—An Exercise in A²I. Challenges of Software Verification. Intelligent Systems Reference Library 238. Springer 2023, pp. 157-179
• Simmo Saan, Michael Schwarz, Julian Erhard, Manuel Pietsch, Helmut Seidl, Sarah Tilscher, Vesal Vojdani. Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution). TACAS (2) 2023: 547-552
• Julian Erhard, Simmo Saan, Sarah Tilscher, Michael Schwarz, Karoliine Holter, Vesal Vojdani, Helmut Seidl. Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap. CoRR abs/2209.10445 (2022)

Teaching

• Advanced Concepts of Programming Languages (tutorial): WiSe21, WiSe22, WiSe23
• Compiler Construction (tutorial): SoSe22, SoSe23
• The Tyranny of Types: Curse or Blessing (seminar): SoSe22
• Static Analysis - Tools and Techniques (seminar): WiSe23

Student Theses

If you are interested in doing a student thesis related to static analysis and Goblint, its web frontend GobView or the verification of fixpoint algorithms in Isabelle, feel free to reach out. For more information on possible student topics see here.

In Progress:

• Towards the Verification of Top-Down Solvers (master thesis)

Finished:

• Automatic Generation of Test Cases for lncremental Static Analysis (bachelor thesis, 8/23)
• Visualizing Non-local Static Analysis Results in GobView (bachelor thesis, 8/23)
• GobView - Making Static Analysis Results Understandable (bachelor thesis, 7/23)
• Control-Flow Graph Matching for Incremental Static Analysis in Goblint (bachelor thesis, 11/22)
• Towards Zero-Cost Reanalysis of Programs after Common Refactorings (bachelor thesis, 08/22)