2026-07-26T07:56:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17088 2024-09-27T06:39:01Z ddc:004 open_access

Towards Concurrent Quantitative Separation Logic Fesefeldt, Ira Katoen, Joost-Pieter Noll, Thomas Randomization Pointers Heap-Manipulating Separation Logic Concurrency 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ira Fesefeldt and Joost-Pieter Katoen and Thomas Noll 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.25 urn:nbn:de:0030-drops-170881 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.25 eng https://creativecommons.org/licenses/by/4.0/legalcode