Foto von Michael Schwarz

Michael Schwarz, M.Sc.

Since 2019, I am a PhD candidate in Helmut Seidl's group and a participant in the DFG Research Training Group ConVeY (Continous Verification of Cyber-Physical Systems).
I am interested in Static Analysis and currently work within the field of Sound Static Analysis by Abstract Interpretation. There, we have, e.g., proposed techniques for efficient abstract interpretation of multi-threaded programs, worked on increasing usability by making static analysis incremental, and designed novel analyses for sometimes overlooked features of the C programming language. I contribute to and currently co-maintain (with Simmo Saan from UTartu) the static analysis framework Goblint for multi-threaded C programs, which serves as the testbed for many of our ideas.
I received a B.Sc. from TUM in 2016, and a M.Sc. from TUM in 2019. During my Master's, I spent one term on exchange at the University of Waterloo and interned at NTNU as a software engineer for one term.

Publications

  • M. Schwarz, H. Seidl: Octagons Revisited: Elegant Proofs and Simplified Algorithms. SAS 2023 (to appear)
  • M. Schwarz, S. Saan, H. Seidl, J. Erhard, V. Vojdani: Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. ESOP 2023: 28-58 (paper, artifact, extended preprint with proofs)
  • M. Schwarz, J. Erhard, V. Vojdani, S. Saan, H. Seidl: When Long Jumps Fall Short: Control-Flow Tracking and Misuse Detection for Non-local Jumps in C. SOAP@PLDI 2023: 20-26 (paper, artifact)
  • S. Tilscher, Y. Stade, M. Schwarz, R. Vogler, H. Seidl: The Top-Down Solver—An Exercise in A2I. Challenges of Software Verification. Intelligent Systems Reference Library 238: 157-179 (paper)
  • S. Saan, M. Schwarz, J. Erhard, M. Pietsch, H. Seidl, S. Tilscher, V. Vojdani: Goblint: Autotuning Thread-Modular Abstract Interpretation - (Competition Contribution). TACAS (2) 2023: 547-552 (paper)
  • J. Erhard, S. Saan, S. Tilscher, M. Schwarz, K. Holter, V. Vojdani, H. Seidl: Interactive Abstract Interpretation: Reanalyzing Whole Programs for Cheap. (under review, preprint, artifact)
  • M. Schwarz, S. Saan, H. Seidl, K. Apinis, J. Erhard, V. Vojdani: Improving Thread-Modular Abstract Interpretation. SAS 2021: 359-383 (paper, artifact, extended preprint with proofs)
  • S. Saan, M. Schwarz, K. Apinis, J. Erhard, H. Seidl, R. Vogler, V. Vojdani: Goblint: Thread-Modular Abstract Interpretation Using Side-Effecting Constraints - (Competition Contribution). TACAS (2) 2021: 438-442 (paper)

Service

  • Artifact Evaluation Committee - TACAS'22
  • Outreach: TEDxTUM (student-organized popular science conference) Licensee 2019-2022

Teaching

Classes:

Before starting as a PhD student, I worked part-time as an undergrad TA, winning awards for best student TA (Preis für die beste Lehre der Fakultät für Informatik) in 2015, 2016, and 2017. 

Supervised Theses:
I currently do not have the capacity to supervise any additional students. If you are interested in doing a student thesis related to static analysis and Goblint, feel free to reach out to my colleagues Sarah Tilscher and Julian Erhard. For more information on possible student topics see here.

Bachelor's Theses Master's Theses
  • String Abstract Domains for the Static Analyzer Goblint (Nathan Schmidt, 08/23)
  • Combatting the Precision Loss of Partial Contexts in Abstract Interpretation (Felix Krayer, 02/23)
  • Automatic Configuration of Goblint - Tuning for Efficient, Yet Precise Enough Analyses of Programs (Manuel Pietsch, 09/22, resulting in joint publication at SVCOMP '23)
  • Increasing the Precision of the Static Analyzer Goblint by Loop Unrolling (Mireia Cano Pujol, 02/22)
  • Towards an integration of Sarif into Goblint (Alexander Eichler, 10/21)
  • A Continuous Integration and Testing Platform for the Static Analyzer Goblint (Andreas Ferrano, 04/21)
  • Webtool to create and check canonical LR automata (Leo Fahrbach, 02/21, co-supervised with Dr. Michael Petter)
  • Extending a Syntactic Search in C Source Code with Analysis Results from the Static Analyzer Goblint (Elias Brandstetter, 09/20)
  • Extending a VS-Code Plugin for a LLVM-based Program Analyzer with a Mapping back to High Level Code (Benedikt Kehrein, 09/20)
  • Comparison of Analyses in CIL and Goblint (Kerem Cakirer, 09/20)
  • Syntactical Search in C Source Code (Olga Faddeenkov, 07/20)
  • User Interface for Program Analyzer Goblint using a OCaml-JavaScript Transpiler (Alex Micheli, 05/20)
  • Local Traces: Partial Order Reduction for Free (Olga Faddeenkov, 05/23)
  • Implementing and Comparing Linear Relational Domains in the Static Analyzer Goblint (Martin Wehking, 05/22)
  • Improved Abstract Domains for Structs in the Static Analyzer Goblint (Jakob Erzar, 10/21)
  • Liveness Analysis of Multi-Threaded C with Posix Threads (Denis Grebennicov, 05/21)
  • Implementation and Comparison of Precision of Various Abstract Domains in the Program Analyzer Goblint (Dymtro Yakymets, 11/20)

 

Guided Research

  • Interactive Abstract Intepretation (Kerem Cakirer, 05/22)