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
2021
[bibtex] @conference{ACCBCHRG2021, title = {Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars}, author = {Ira Justus Fesefeldt and Christoph Matheja and Thomas Noll and Johannes Schulte}, publisher = {Springer}, booktitle = {LNCS}, volume = {12741}, pages = {283-293}, type = {Conference Paper}, year = {2021}, doi = {10.1007/978-3-030-78946-6_15}, url = { https://publications.rwth-aachen.de/record/820755}, }× [issue]	Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte. Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, 14. International Conference on Graph Transformation (ICGT21), Volume 12741 of LNCS, 283-293, Springer, 2021.
2019
[bibtex] @masterthesis{P2019, title = {Proving termination of pointer programs on top of symbolic execution}, author = {Ira Justus Fesefeldt}, institution = {RWTH Aachen University}, pages = {118 S.}, type = {Master Thesis}, year = {2019}, doi = {10.18154/RWTH-2020-04970}, url = { https://publications.rwth-aachen.de/record/789066}, }× [issue]	Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen University, 118 S., 2019.