- fesefeldt at cs.rwth-aachen.de
- Room 4210
- +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”.
I am looking for a student assistant job for implementing various graph based symbolic execution algorithms for analyzing programs on data structures. Being comfortable with formal methods are requires
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.
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).
I am currently supervising the following thesis projects:
- Alexander Ferber, Combining Integer Programs and Graph Grammars: Theory and Implementation in Attestor, Bachlor’s Thesis
I have supervised the following thesis projects:
- 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
I’m currently involved in the following teaching activities:
- Theoretical Foundations of UML (WS23)
I was involved in the following teaching activities:
- Datenstrukturen und Algorithmen (SS23)
|[bibtex] [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.|
|[bibtex] [issue]||Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, , 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] [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] [issue]||Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, -62, 2022. https://arxiv.org/abs/2207.02822|