A simple abstraction for complex concurrent indexes. - Pedro da Rocha Pinto; Thomas Dinsdale-Young; Mike Dodds; Philippa Gardner; Mark J. Wheelhouse (OOPSLA, 2011)

TaDA: A Logic for Time and Data Abstraction. - Pedro da Rocha Pinto; Thomas Dinsdale-Young; Philippa Gardner (ECOOP, 2014)

Fault-Tolerant Resource Reasoning. - Gian Ntzik; Pedro da Rocha Pinto; Philippa Gardner (APLAS, 2015)

Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). - Pedro da Rocha Pinto; Thomas Dinsdale-Young; Philippa Gardner (MFPS, 2015)

Modular Termination Verification for Non-blocking Concurrency. - Pedro da Rocha Pinto; Thomas Dinsdale-Young; Philippa Gardner; Julian Sutherland (ESOP, 2016)

Reasoning with time and data abstractions. - Pedro da Rocha Pinto (2016)

Caper - Automatic Verification for Fine-Grained Concurrency. - Thomas Dinsdale-Young; Pedro da Rocha Pinto; Kristoffer Just Andersen; Lars Birkedal (ESOP, 2017)

Abstract Specifications for Concurrent Maps. - Shale Xiong; Pedro da Rocha Pinto; Gian Ntzik; Philippa Gardner (ESOP, 2017)

A Concurrent Specification of POSIX File Systems. - Gian Ntzik; Pedro da Rocha Pinto; Julian Sutherland; Philippa Gardner (ECOOP, 2018)

A perspective on specifying and verifying concurrent modules. - Thomas Dinsdale-Young; Pedro da Rocha Pinto; Philippa Gardner (J. Log. Algebraic Methods Program., 2018)