### 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. Formal proofs provide 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 is a proof 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.

## 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

## Implementation of a theorem prover microkernel

*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. Formal proofs provide 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 is a proof system supporting safety reasoning about cyber-physical systems.

In this thesis, the logic dLCHP is to be implemented as an extension of the interactive proof assistant KeYmaeara X for hybrid systems.

**Requirements:** The student should have experience in functional programming (e.g. Haskell, Scala) and modern web frameworks (e.g. Angular, React)

## Formalization of Game Logic with Sabotage in Isabelle/HOL

*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**: Game logic with sabotage (GLs) [1] studies the abilities of competing agents to reach their goals if they can be so mean to lay traps for each other. Unlike game logic without sabotage, GLs is equiexpressive to the modal mu-calculus (L-mu), a logic that can be used to characterize important formal methods e.g. model checking. By equiexpresisvenss GLs provides a novel perspective onto these formal methods. Further, the equiexpressivenss is the foundation for the first completeness result for game logic. Recent flaws in related proofs make the formal verification of this proof a significant task.

In this thesis, the equiexpressivness of GLs and the L-mu is to be formalized in the proof assistant Isabelle/HOL.

**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.

## 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

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