Ira Fesefeldt

dblp:296/0440 · DBLP profile ↗
← Back
3ranked-venue papers
2as first author
3since 2021 · last 2022
0000-0001-7837-2611ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Theory of computation · 2 · 2 first-author · 2 since 2021Software engineering, systems software and programming languages · 1 · 1 since 2021Databases, data management, data science and information retrieval · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2022 Towards Concurrent Quantitative Separation Logic
Ira Fesefeldt, Joost-Pieter Katoen, Thomas Noll 0001
CONCUR1
2022 Foundations for Entailment Checking in Quantitative Separation Logic
abstract
Abstract Quantitative separation logic () is an extension of separation logic () for the verification of probabilistic pointer programs. In , formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with , one of the key problems when reasoning with is entailment: does a formula f entail another formula g? We give a generic reduction from entailment checking in to entailment checking in . This allows to leverage the large body of research for the automated verification of probabilistic pointer programs. We analyze the complexity of our approach and demonstrate its applicability. In particular, we obtain the first decidability results for the verification of such programs by applying our reduction to a quantitative extension of the well-known symbolic-heap fragment of separation logic.
Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll 0001
ESOP2
2021 Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
Ira Fesefeldt, Christoph Matheja, Thomas Noll 0001, Johannes Schulte
ICGT1