Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs

Abstract

We present quantitative separation logic ($\mathsf{QSL}$). In contrast to classical separation logic, $\mathsf{QSL}$ employs quantities which evaluate to real numbers instead of predicates which evaluate to Boolean values. The connectives of classical separation logic, separating conjunction and separating implication, are lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, e.g. modus ponens, adjointness, etc. Furthermore, we develop a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in $\mathsf{QSL}$. This calculus is a conservative extension of both Reynolds' separation logic for heap-manipulating programs and Kozen's / McIver and Morgan's weakest preexpectations for probabilistic programs. Soundness is proven with respect to an operational semantics based on Markov decision processes. Our calculus preserves O'Hearn's frame rule, which enables local reasoning. We demonstrate that our calculus enables reasoning about quantities such as the probability of terminating with an empty heap, the probability of reaching a certain array permutation, or the expected length of a list.

References in corpus (2)

• A Separation Logic for Concurrent Randomized Programs
• A New Proof Rule for Almost-Sure Termination

Cited by in corpus (16)

• Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
• Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
• A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
• Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
• A Separation Logic for Negative Dependence
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
• Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
• Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
• On Algebraic Abstractions for Concurrent Separation Logics
• Tachis: Higher-Order Separation Logic with Credits for Expected Costs
• Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
• J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
• Symbolic Quantitative Information Flow for Probabilistic Programs
• Reasoning about Recursive Quantum Programs