We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 2024!

Marvin Brieger

Picture of 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
E-Mail
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
Case Studies in the Dynamic Logic of Communicating Hybrid Programs

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