Foundations for Entailment Checking in Quantitative Separation Logic (extended version)

TL;DR

This paper introduces a reduction from entailment checking in quantitative separation logic (QSL) to classical separation logic (SL), enabling the use of existing SL tools for verifying probabilistic pointer programs, and provides initial decidability results.

Contribution

It presents the first generic reduction from QSL entailment to SL entailment, facilitating automated verification of probabilistic pointer programs.

Findings

Reduction enables leveraging SL verification tools for QSL.

Complexity analysis of the reduction.

Decidability results for a fragment of QSL.

Abstract

Quantitative separation logic (QSL) is an extension of separation logic (SL) for the verification of probabilistic pointer programs. In QSL, formulae evaluate to real numbers instead of truth values, e.g., the probability of memory-safe termination in a given symbolic heap. As with \SL, one of the key problems when reasoning with QSL is \emph{entailment}: does a formula f entail another formula g? We give a generic reduction from entailment checking in QSL to entailment checking in SL. This allows to leverage the large body of SL 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.