eprintid: 10089701
rev_number: 23
eprint_status: archive
userid: 608
dir: disk0/10/08/97/01
datestamp: 2020-01-29 08:34:28
lastmod: 2021-10-19 22:21:41
status_changed: 2020-01-29 08:34:28
type: article
metadata_visibility: show
creators_name: Batz, K
creators_name: Kaminski, BL
creators_name: Katoen, J-P
creators_name: Matheja, C
creators_name: Noll, T
title: Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
ispublished: pub
divisions: UCL
divisions: B04
divisions: C05
divisions: F48
note: © 2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 license.
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.
date: 2019-01
official_url: http://dx.doi.org/10.1145/3290347
oa_status: green
full_text_type: pub
language: eng
primo: open
primo_central: open_green
verified: verified_manual
elements_id: 1741700
doi: 10.1145/3290347
lyricists_name: Kaminski, Benjamin
lyricists_id: BKAMI07
actors_name: Waragoda Vitharana, Nimal
actors_id: NWARR44
actors_role: owner
full_text_status: public
publication: Proceedings of the ACM on Programming Languages
volume: 3
article_number: 34
citation:        Batz, K;    Kaminski, BL;    Katoen, J-P;    Matheja, C;    Noll, T;      (2019)    Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs.                   Proceedings of the ACM on Programming Languages , 3     , Article 34.  10.1145/3290347 <https://doi.org/10.1145/3290347>.       Green open access   
 
document_url: https://discovery.ucl.ac.uk/id/eprint/10089701/1/Kaminski_3290347.pdf