Ira Fesefeldt

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

Research

My research interests include:

  • formal verification of probabilistic, heap-manipulating and concurrent programs,
  • separation logics,
  • termination analysis,
  • static program analysis, and
  • graph-grammars.

I was involved in reviews for:

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

Supervision

I am currently supervising 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)


I have supervised the following thesis projects:


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

  • Datenstrukturen und Algorithmen (SS23)



I was involved in the following teaching activities:



Publications

2022
DOI fulltext PDF [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.
DOI fulltext PDF [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.
DOI arXiv:2207.02822 fulltext PDF [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
DOI [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.
Show all