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

Job Offers

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.

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