[Shale Xiong](https://psvg.doc.ic.ac.uk/people/xiong.html), [Pedro Da Rocha Pinto](https://psvg.doc.ic.ac.uk/people/da-rocha-pinto.html),
[Gian Ntzik](https://psvg.doc.ic.ac.uk/people/ntzik.html) and [Philippa Gardner](https://psvg.doc.ic.ac.uk/people/gardner.html)
have had a paper accepted at [ESOP 2017]9http://www.etaps.org/index.php/2017/esop),
entitled [Abstract Specifications for Concurrent Maps](https://psvg.doc.ic.ac.uk/publications/Xiong2017Abstract.html).
The paper 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.
Pedro Da Rocha Pinto, in collaboration with [Thomas Dinsdale-Young](http://cs.au.dk/~tyoung/),
[Kristoffer Just Andersen](http://pure.au.dk/portal/en/persons/id(5e842a19-8b76-487a-8082-06b6d6ff2545).html)
and [Lars Birkedal](http://www.cs.au.dk/~birke/) from Aarhus University, has had a paper accepted at ESOP 2017, entitled Caper: Automatic Verification for Fine-grained Concurrency.
This 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.
