RGSep Action Inference
RGSep Action Inference
复制标题
RGSep 动作推理
DOI：
10.1007/978-3-642-11319-2_25
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Viktor Vafeiadis
中科院分区：
文献类型：
--
作者：
Viktor Vafeiadis
我们提出了一种基于 RGSep 的自动验证过程，适用于细粒度并发堆操作程序的推理。该过程计算一组 RGSep 操作，过度近似每个线程对其并发环境造成的干扰。这些推断的操作使我们能够验证文献中一系列实用并发算法的安全性、活性和功能正确性。
We present an automatic verification procedure based on RGSep that is suitable for reasoning about fine-grained concurrent heap-manipulating programs. The procedure computes a set of RGSep actions overapproximating the interference that each thread causes to its concurrent environment. These inferred actions allow us to verify safety, liveness, and functional correctness properties of a collection of practical concurrent algorithms from the literature.