Email

fesefeldt at cs.rwth-aachen.de

Address

Room 4210
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21204

I was a PhD student in the Software Modeling and Verification Group headed by Professor J.-P. Katoen. I am currently working at mgm GmbH in Aachen, Germany on software in the public sector.

If you write me a Mail, please refrain from using a gendered address, or if absolutely necessary, use “Ms” or “Frau”.

Research

My research interests include:

• formal verification of probabilistic, heap-manipulating and concurrent programs,
• separation logics,
• termination analysis,
• static program analysis,
• graph-grammars and
• proof assistants such as lean, coq and iris.

I was involved in reviews for:

• CAV 2022 (external reviewer),
• POPL 2023 (external reviewer),
• FM 2023 (external reviewer and external AE reviewer),
• CAV 2023 (AE reviewer), and
• TACAS 2025 (external reviewer).

Supervision

I’m currently not involved in teaching activities.

I was involved in the following teaching activities:

• Proseminar Datenstrukturen und Algorithmen (SS24)

• Theoretical Foundations of UML (WS23)

• Seminar Deductive Verification (WS23)

• Datenstrukturen und Algorithmen (SS23)

• Compiler Construction (WS22)

• Seminar Probabilistic Programming (WS22)

• Datenstrukturen und Algorithmen (SS22)

• Seminar: Advanced Topics in Formal Semantics (WS21)

• Datenstrukturen und Algorithmen (SS21)

• Compiler Constructions (WS20)

• Proseminar: Algorithmen und Datenstrukturen (WS20)

• Datenstrukturen und Algorithmen (SS20)

• Proseminar: Introduction to Program Analysis (SS20)

I have supervised the following thesis projects:

• Patrick Arens, MARVEL: A stepwise Debugging Tool for Markov Models in the PRISM-Language, Master’s Thesis

• Patrick Nossol, Entailments in Quantitative Separation Logic with Recursive Definitions: Constructing Cyclic Proofs, Master’s Thesis

• Alexander Ferber, Combining Integer Programs and Graph Grammars: Theory and Implementation in Attestor, Bachlor’s Thesis

• Jan Tugsbayar, Verification of Leader Election Protocols in Unreliable Networks, Bachelor’s Thesis (advising together with Prof. Thomas Noll)

• Dominic Meiser, Design and Evaluation of a Probabilistic Pointer Programming Language using Monte-Carlo Simulation, Bachelor’s Thesis (advising together with Prof. Thomas Noll)

• Mohamed Khalifa, Termination Analysis of Procedural Pointer Programs Modelled by Graph Grammars, Master’s Thesis

• Fabian Gasser, Analysis of Concurrent Probabilistic Programs with Shared Variables, Bachelor’s Thesis (advised together with Prof. Thomas Noll)

• Marvin Jansen, Decidability and complexity of entailment checking in quantitative separation logic, Master’s Thesis, winner of the CS Department Award 2021 (advised togehter with Kevin Batz and Dr. Christoph Matheja)

• Patrick Arens, Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs, Bachelor’s Thesis

• Mohamed Khalifa, Implementation of a predicate-guided termination analysis for pointer programs, Bachelor’s Thesis

Publications