Bi-Weekly Talk: Quantitative Separation Logic

Wednesday, June 27, 2018, 10:15 am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10


Speaker: Benjamin Kaminski


We present quantitative separation logic. In contrast to classical separation logic, quantitative separation logic 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 both lifted from predicates to quantities. This extension is conservative: Both connectives are backward compatible to their classical analogs and obey the same laws, for example, modus ponens, adjointness of separating conjunction and separating implicaiton, and so on. Furthermore, we develop a weakest precondition calculus for quantitative reasoning about probabilistic pointer programs in quantitative separation logic. This calculus is a conservative extension of both Reynolds' weakest preconditions for heap manipulating programs and McIver & Morgan's weakest preexpectations for probabilistic programs. Soundness is proven with respect to an operational semantics based on Markov decision processes. Moreover, our calculus preserves O'Hearn's frame rule which enables local reasoning - a key principle of separation logic.