ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sun 7 Apr 2019 16:00 - 16:30 at S7 - Session IV

This is a presentation report. We present quantitative separation logic (QSL). In contrast to classical separation logic, 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 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’sframe rule, which enables local reasoning.

Sun 7 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00
Session IVQAPL at S7
16:00
30m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
QAPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
DOI
16:30
30m
Talk
An Adequate Semantics for Hybrid While
QAPL
Sergey Goncharov FAU Erlangen-Nürnberg, Lehrstuhl 8, Renato Neves University of Minho & INESC TEC
17:00
30m
Talk
Recent Applications and Quantitative Aspects of Spatial Model Checking
QAPL
17:30
30m
Talk
Equational Characterization Metaresults for Bisimulation and Trace Semantics in ULTraS
QAPL
Marco Bernardo University of Urbino