License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2022.25
URN: urn:nbn:de:0030-drops-170881
Go to the corresponding LIPIcs Volume Portal

Fesefeldt, Ira ; Katoen, Joost-Pieter ; Noll, Thomas

Towards Concurrent Quantitative Separation Logic

LIPIcs-CONCUR-2022-25.pdf (0.9 MB)


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.

BibTeX - Entry

  author =	{Fesefeldt, Ira and Katoen, Joost-Pieter and Noll, Thomas},
  title =	{{Towards Concurrent Quantitative Separation Logic}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{25:1--25:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-170881},
  doi =		{10.4230/LIPIcs.CONCUR.2022.25},
  annote =	{Keywords: Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency}

Keywords: Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency
Collection: 33rd International Conference on Concurrency Theory (CONCUR 2022)
Issue Date: 2022
Date of publication: 06.09.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI