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
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17088/
Fesefeldt, Ira ;
Katoen, Joost-Pieter ;
Noll, Thomas
Towards Concurrent Quantitative Separation Logic
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.
BibTeX - Entry
@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.dagstuhl.de/opus/volltexte/2022/17088},
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 |
