Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 11:19 - 11:41 at Sala I - Reasoning about Probabilistic Programs Chair(s): Jan Hoffmann

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 Ishtiaq’s, O’Hearn’s, and 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.

Quantitative Separation Logic - Slides (qsl-slides.pdf)1.73MiB

Wed 16 Jan

10:35 - 12:03: Research Papers - Reasoning about Probabilistic Programs at Sala I
Chair(s): Jan HoffmannCarnegie Mellon University
POPL-2019-Research-Papers10:35 - 10:57
Tetsuya SatoUniversity at Buffalo, SUNY, USA, Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Justin HsuUniversity of Wisconsin-Madison, USA
Link to publication DOI File Attached
POPL-2019-Research-Papers10:57 - 11:19
Joseph TassarottiCarnegie Mellon University, Robert Harper
Link to publication DOI File Attached
POPL-2019-Research-Papers11:19 - 11:41
Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaRWTH Aachen University, Thomas NollRWTH Aachen University
Link to publication DOI File Attached
POPL-2019-Research-Papers11:41 - 12:03
Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison
Link to publication DOI