RGSep Action Inference

We present an automatic verification procedure based on RGSep that is suitable for reasoning about fine-grained concurrent heapmanipulating 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.

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Viktor Vafeiadis
• Keywords: Automatic Verification Procedure, Fine-grained Concurrent Heapmanipulating, Practical Concurrent Algorithms, Software Engineering, VMCAI 2010