Foto von Michael Schwarz

Michael Schwarz, M.Sc.

For inquiries relating to IN003 (Functional Programming and Verification) please email ONLY our shared mailbox fpv@in.tum.de.

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 and Karoliine Holter 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

Highlighted (ordered chronologically)
  • S. Saan, M. Schwarz, J. Erhard, H. Seidl, S. Tilscher, V. Vojdani: Correctness Witness Validation by Abstract Interpretation. VMCAI 2024: 74-97 (paper, artifactpreprint,  won Best Paper Award)
  • M. Schwarz, H. Seidl: Octagons Revisited: Elegant Proofs and Simplified Algorithms. SAS 2023: 485-507 (paper)
  • 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)
  • 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, 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)
Others (ordered chronologically)
  • 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 (paper)
  • 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 (paper)
  • 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)
  • 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)
  • 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)
  • 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)
  • 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

  • Reviewer - STTT Special Section CSV'23
  • Artifact Evaluation Committee - SAS '24, ESOP/FASE/FoSSaCS '24, 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
  • Witnessing Violations of Safety Properties for Concurrent Programs (Sofiia Danylchenko, 10/23)
  • 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)
  • Certifying Memory Safety of Concurrent Programs by Abstract Interpretation (Stanimir Bozhilov, 10/23, resulting in two joint publications at SVCOMP'24)
  • 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)