Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Dinsdale-Young:2018:10.1016/j.jlamp.2018.03.003,
author = {Dinsdale-Young, TW and da, Rocha Pinto P and Gardner, PA},
doi = {10.1016/j.jlamp.2018.03.003},
journal = {Journal of Logical and Algebraic Methods in Programming},
pages = {1--25},
title = {A perspective on specifying and verifying concurrent modules},
url = {http://dx.doi.org/10.1016/j.jlamp.2018.03.003},
volume = {98},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - The specification of a concurrent program module, and the verification of implementations and clients with respect to such a specification, are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We 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.
AU  - Dinsdale-Young,TW
AU  - da,Rocha Pinto P
AU  - Gardner,PA
DO  - 10.1016/j.jlamp.2018.03.003
EP  - 25
PY  - 2018///
SN  - 2352-2208
SP  - 1
TI  - A perspective on specifying and verifying concurrent modules
T2  - Journal of Logical and Algebraic Methods in Programming
UR  - http://dx.doi.org/10.1016/j.jlamp.2018.03.003
UR  - http://hdl.handle.net/10044/1/58595
VL  - 98
ER  -
Download