- Pedro da Rocha Pinto
- Thomas Dinsdale-Young
- Philippa Gardner
The specification of a concurrent program module is a difficult problem. The specifications must be strong enough to enable reasoning about the intended clients without reference to the underlying module implementation. We survey a range of verification techniques for specifying concurrent modules, in particular highlighting four key concepts: auxiliary state, interference abstraction, resource ownership and atomicity. We show how these concepts combine to provide powerful approaches to specifying concurrent modules.
Electr. Notes Theor. Comput. Sci., vol. 319, pp. 3–18