Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)


  • 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

Publication Date

Jun 2015


Source Materials