1 Search Results for "Noll, Thomas"


Document
Towards Concurrent Quantitative Separation Logic

Authors: Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


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.

Cite as

Ira Fesefeldt, Joost-Pieter Katoen, and Thomas Noll. Towards Concurrent Quantitative Separation Logic. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 25:1-25:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{fesefeldt_et_al:LIPIcs.CONCUR.2022.25,
  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 =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.25},
  URN =		{urn:nbn:de:0030-drops-170881},
  doi =		{10.4230/LIPIcs.CONCUR.2022.25},
  annote =	{Keywords: Randomization, Pointers, Heap-Manipulating, Separation Logic, Concurrency}
}
  • Refine by Author
  • 1 Fesefeldt, Ira
  • 1 Katoen, Joost-Pieter
  • 1 Noll, Thomas

  • Refine by Classification
  • 1 Mathematics of computing → Probabilistic reasoning algorithms
  • 1 Theory of computation → Concurrent algorithms
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Concurrency
  • 1 Heap-Manipulating
  • 1 Pointers
  • 1 Randomization
  • 1 Separation Logic

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail