Towards Concurrent Quantitative Separation Logic

arXiv (Cornell University)

Abstract

In this paper, we develop a novel verification technique to reason about programs featuring concurrency, pointers and randomization. While the integration of concurrency and pointers is well studied, little is known about the combination of all three paradigms. To close this gap, we combine two kinds of separation logic - Quantitative Separation Logic and Concurrent Separation Logic - into a new separation logic that enables reasoning about lower bounds of the probability to realise a postcondition by executing such a program.

Authors 3

1. Ira Fesefeldt Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen

3. Thomas Noll Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen