Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming (ESOP 2017), which will take place this April in Uppsala, Sweden. The first paper, Abstract Specifications for Concurrent Maps, present the importance of abstract atomicity for reasoning fine-grained concurrent modules. The second paper, Caper: Automatic Verification for Fine-grained Concurrency, presents a prototype tool for automated reasoning about concurrent modules.

The first paper, submitted by Shale Xiong, Pedro Da Rocha Pinto, Gian Ntzik and Philippa Gardner, Abstract Specifications for Concurrent Maps demonstrates that abstract atomicity is key to give a specification for concurrent map that allows better client reasoning. This paper also provides the first functional correctness proof of ConcurrentSkiplistMap in java.util.concurrent with respect to the abstract specification.

The second paper accepted, submitted by Pedro Da Rocha Pinto, in collaboration with Thomas Dinsdale-Young, Kristoffer Just Andersen and Lars Birkedal from Aarhus University is Caper: Automatic Verification for Fine-grained Concurrency. The paper presents Caper, a prototype tool for automated reasoning about concurrent modules. Caper is based on symbolic execution, integrating reasoning about interference on shared resources. This enables Caper to verify the functional correctness of fine-grained concurrent modules.