A paper co-authored by current and former researchers of the group has just been publised. A second paper, also collaborative work with current and former researchers has also just been accepted to ECOOP 18.
The first paper, A perspective on specifying and verifying concurrent modules by Thomas Dinsdale-Young, Pedro da Rocha Pinto and Philippa Gardner has been published in the Journal of Logical and Algebraic Methods in Programming.
In the paper, the authors survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. They highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. Then they demonstrate how these concepts can be combined to achieve two powerful approaches for specifying concurrent modules and verifying implementations and clients, which remove the limitations highlighted by the counter example.
The second paper, co-authored by Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland and Philippa Gardner has just been accepted to the 32nd European Conference on Object-Oriented Programming (ECOOP 2018), which will be held in Amsterdam in July.
In the paper, entitled A Concurrent Specification of POSIX File Systems, the authors provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients.
Congratulations to all.