Foundations for Entailment Checking in Quantitative Separation Logic
Lecture notes in computer science, pp. 57–84
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.
Authors 7
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
-
Christoph Matheja corresponding
ETH Zurich · Technical University of Denmark
Affiliation as printed
Programming Methodology Group, ETH Zürich, Zürich, Switzerland
Technical University of Denmark, Lyngby, Denmark
-
Affiliation as printed
Software Modeling and Verification Group, RWTH Aachen University, Aachen, Germany
Cited by 4 stored of 4
4 results
No patents citing this paper on Lens.org (checked 2026-10-06).