Marvin Brieger
Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538
Munich
(Germany)
- Office
- Room F 009, Oettingenstr. 67
- firstname.lastname@sosy.ifi.lmu.de
- Office Hours
- By appointment
- Personal Homepage
- marvinbrieger.de
- ORCID
- 0000-0001-9656-2830
GPG-Key
Please send me encrypted mails!
My GPG key: 0xF52541AF5BCA78FC
Fingerprint: D877 F639 6831 5FB9 91FC 40B5 F525 41AF 5BCA 78FC
Thesis Mentoring
Available topics
Formalization of Communicating Hybrid Systems Axiomatics in Isabelle/HOL
This topic is available as a BSc thesis, a MSc thesis, or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.
Goal: The safe interaction of computers with their physical environment (e.g. in modern car-controllers or care robots) requires utmost care as human health and life may be directly affected by a malfunction. Logical reasoning about such systems provides a very high level of certainty about the safety of such cyber-physical systems. The dynamic logic of communicating hybrid programs (dLCHP), which describes interactions of computers, physical behavior, communication, and parallelism, is one logical system supporting safety reasoning about cyber-physical systems.
In this thesis, parts of the theory of dLCHP are to be formalized in the interactive proof assistant Isabelle/HOL. That is, available pen-and-paper proofs are to be carried over into a mechanized theory in the proof assistant.
Requirements: The student must already have experience in using an interactive theorem prover (e.g. Isabelle/HOL, Coq, Lean), which might have been obtained in a lecture, seminar, or practical course.
Finished topics
If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.
Research
My research develops logic-based methods for the safety analysis of concurrent cyber-physical systems (CPSs). More precisely, I study extensions of differential dynamic logic (dL) to concurrency. Ultimately, I aim to extend the theorem prover KeYmaera X with proof calculi for logics of concurrent CPSs to support the interactive verification of their safety.
My PhD advisor is André Platzer.
Publications
Please check out my personal research webpage: marvinbrieger.de.
Teaching
- WS 2023/24: Bachelor-Seminar: Verifikation von Programmen mit Schleifen und Arrays
- WS 2023/24: Master-Vorlesung: Projektmanagement (im Elite-Master Sofwareengineering)
- SS 2023: Bachelor-Seminar: Formale Methoden für Cyber-Physical Systems
- WS 2022/23: Bachelor-Seminar: Formale Methoden für Cyber-Physical Systems
- WS 2022/23: Master-Vorlesung: Projektmanagement (im Elite-Master Sofwareengineering)
- SS 2022: Bachelor-Seminar: Programmsynthese