Fakult?tskolloquium am 07. November 2019, 16 Uhr, WE5/05.003

Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Pointer Programs Separation Logic (SL) has been developed as an enhancement to classical Hoare Logic that supports modular reasoning about pointer programs. In this talk we present Quantitative Separation Logic (QSL), which provides a conservative extension of SL by evaluating formulae to real numbers rather than Boolean values. To this aim, SL connectives such as separating conjunction and separating implication are lifted from predicates to quantities.

Furthermore, we develop a weakest precondition calculus for probabilistic pointer programs using QSL, and demonstrate that it 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 size of a dynamic data structure.