Email

fesefeldt at cs.rwth-aachen.de

Address

Room 4210
Ahornstraße 55
D-52074 Aachen

Phone

+49 241 80 21204

I am a PhD student in the Software Modeling and Verification Group headed by Professor J.-P. Katoen.

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

Job Offers

I am looking for a student assistant job for a Hoare-style proof systems of probabilistic programs in the proof assistant Lean. It is required to be able to be comfortable formally proving theorems.

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), and
• CAV 2023 (AE reviewer).

Supervision

I am currently supervising the following thesis projects:

• Patrick Nossol, QSL Entailments using Cyclic Proofs (working title), Master’s Thesis

• Patrick Arens, Operational Probabilistic Debugger (working title), Master’s Thesis

I have supervised the following thesis projects:

• 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

Teaching

I’m currently involved in the following teaching activities:

• Proseminar Datenstrukturen und Algorithmen (SS24)

I was involved in the following teaching activities:

• 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)

Publications

2023
[bibtex] @proceedings{KPGP2023, title = {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung}, author = {}, editor = {Thomas Noll and Ira Justus Fesefeldt}, publisher = {RWTH Aachen University, Department of Computer Science}, booktitle = {Aachener Informatik-Berichte}, volume = {AIB-2023-03}, pages = {1 Online-Ressource}, type = {Proceeding Article}, year = {2023}, doi = {10.18154/RWTH-2023-10034}, url = { https://publications.rwth-aachen.de/record/972197}, }× [issue]	Thomas Noll (ed), Ira Justus Fesefeldt (ed). 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung, Volume AIB-2023-03 of Aachener Informatik-Berichte, 1 Online-Ressource, RWTH Aachen University, Department of Computer Science, 2023.
2022
[bibtex] @conference{FECQSL2022, title = {Foundations for Entailment Checking in Quantitative Separation Logic}, author = {Kevin Batz and Ira Justus Fesefeldt and Marvin Jansen and Joost-Pieter Katoen and Florian Keßler and Christoph Matheja and Thomas Noll}, publisher = {Springer}, booktitle = {LNCS}, volume = {13240}, pages = {57-84}, type = {Conference Paper}, year = {2022}, doi = {10.1007/978-3-030-99336-8_3}, url = { https://publications.rwth-aachen.de/record/843799}, }× [issue]	Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll. Foundations for Entailment Checking in Quantitative Separation Logic, 31. European Symposium on Programming (ESOP 2022), Volume 13240 of LNCS, 57-84, Springer, 2022.
[bibtex] @conference{TCQSL2022, title = {Towards Concurrent Quantitative Separation Logic}, author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, booktitle = {LIPIcs - Leibniz International Proceedings in Informatics}, volume = {243}, pages = {25:1-25:24}, type = {Conference Paper}, year = {2022}, doi = {10.4230/LIPICS.CONCUR.2022.25}, url = { https://publications.rwth-aachen.de/record/853299}, }× [issue]	Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, 33. International Conference on Concurrency Theory (CONCUR 2022), Volume 243 of LIPIcs - Leibniz International Proceedings in Informatics, 25:1-25:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
[bibtex] @unpublished{TCQSL2022, title = {Towards Concurrent Quantitative Separation Logic}, author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll}, pages = {[1]-62}, type = {Preprint}, year = {2022}, doi = {10.18154/RWTH-2022-08799}, url = { https://arxiv.org/abs/2207.02822}, }× [issue]	Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, [1]-62, 2022. https://arxiv.org/abs/2207.02822
Show all