论文标题
迈向同时定量分离逻辑
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.
