We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Distinguished Paper Award and Best Artifact Award at FSE 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)

Room
F 009
Office Hours
By appointment
Email
firstname.lastname@sosy.ifi.lmu.de
ORCID
0000-0001-9656-2830
Personal Homepage
marvinbrieger.de

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
Small theorem prover kernels: Uniform substitution for your favorite logic

This topic is available as a MSc thesis or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.

Goal: Uniform substitution is a proof rule that enables the implementation of a theorem prover kernel with very little code. For example, KeYmaera X, a theorem prover for reasoning about Cyber-physical systems, only has 2 kLOC code in its core, while its predecessor KeYmaera not using uniform substitution had 100 kLOC code.

Uniform substitution as a proof rule is always tailor-made for a certain logical system. In this thesis, uniform substitution for some logical system is to be investigated that is not considered yet. For example, uniform substitution could be studied for Incorrectness logic, which can be used for proving presence of bugs in software, or for separation logic, which can be used to reason about pointers.

Requirements: The student should have got good grades in logic and discrete structures and formal specification and verification

Currently assigned 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

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