Towards Concurrent Quantitative Separation Logic
Towards Concurrent Quantitative Separation Logic
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.
Extended version of CONCUR'22 paper
- RWTH Aachen University (Medical Faculty) Germany
- Leibniz Association Germany
- RWTH Aachen University Germany
- Schloss Dagstuhl – Leibniz Center for Informatics Germany
Mathematics of computing ? Probabilistic reasoning algorithms, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Separation Logic, Mathematics of computing → Probabilistic reasoning algorithms, Randomization, Pointers, Heap-Manipulating, 004, Logic in Computer Science (cs.LO), Theory of computation ? Program verification, Theory of computation → Concurrent algorithms, Concurrency, Theory of computation → Program verification, Theory of computation ? Concurrent algorithms, Programming Languages (cs.PL), ddc: ddc:004
Mathematics of computing ? Probabilistic reasoning algorithms, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Programming Languages, Separation Logic, Mathematics of computing → Probabilistic reasoning algorithms, Randomization, Pointers, Heap-Manipulating, 004, Logic in Computer Science (cs.LO), Theory of computation ? Program verification, Theory of computation → Concurrent algorithms, Concurrency, Theory of computation → Program verification, Theory of computation ? Concurrent algorithms, Programming Languages (cs.PL), ddc: ddc:004
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).0 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!