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 the verification of fixpoint algorithms in Isabelle, feel free to reach out. For more information on possible student topics see here.

Open:

• Verification of the Top-Down Solver with Side-Effects in Isabelle (master thesis)
• Evaluating Variants of the Top-Down Solver with the Modular Fixpoint Library ScalaFix (bachelor thesis)

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)