Michael Schwarz, M.Sc.
For inquiries relating to IN003 (Functional Programming and Verification) please email ONLY our shared mailbox fpv@in.tum.de.
- Tel.: +49 (89) 289 - 18182
- Raum: 5607.02.055
- m.schwarz@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, artifact, preprint, 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, extended version to appear in Int. J. Softw. Tools Technol. Transf.)
- 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, S. Tilscher, M. Schwarz: Non-Numerical Weakly Relational Domains. Int. J. Softw. Tools Technol. Transf. (2024) (paper)
- J. Erhard, J.F. Schinabeck, M. Schwarz, H. Seidl: When to Stop Going Down the Rabbit Hole: Taming Context-Sensitivity on the Fly. SOAP@PLDI 2024: 35-44 (paper)
- 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 (3) 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 (3) 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. to appear in Int. J. Softw. Tools Technol. Transf. (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:
- IN0003 Functional Programming and Verification (Winter '21/'22, Summer '22, Summer '23, Summer '24)
("Übungsleitung" together with J. Erhard: Course with ~1000 students; Managing ~20 undergrad TAs and ~4 head TAs, Designing homework and exam, Organizing extra activities; Our head TAs presented part of the course framework at the OCaml Workshop@ICFP: link) - IN2227 Compiler Construction (Summer '20, Summer '21)
- Practical Course: Static Analysis - Automated Bug Hunting and Beyond (Summer '21, Summer '22, Winter '22/'23, Summer '23, Winter '23/'24)
- Practical Course: Program Optimization with LLVM (Winter '19/'20, Summer '20)
- Practical Course: Profiling & Tuning Large Functional Programs (Winter '22/'23)
- Bachelor-Seminar: Static Analysis - Tools and Techniques (Winter '23/'24)
- Master-Seminar: Static Analysis - Mastering Concurrency (Winter '23/'24)
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 |
|
Guided Research
|