Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs

Advanced search
Browse by:

Department | Year

UCL Theses | Latest

Deposit your research

Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs

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. Green open access

Preview

Text
Kaminski_3290347.pdf - Published Version
Download (500kB) | Preview

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.

Type:	Article
Title:	Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Programs
Open access status:	An open access version is available from UCL Discovery
DOI:	10.1145/3290347
Publisher version:	http://dx.doi.org/10.1145/3290347
Language:	English
Additional information:	© 2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 license.
UCL classification:	UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI:	https://discovery.ucl.ac.uk/id/eprint/10089701