Starling: Lightweight Concurrency Verification with Views. - Matt Windsor; Mike Dodds; Ben Simner; Matthew J. Parkinson (CAV (1), 2017)

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures. - Ben Simner; Shaked Flur; Christopher Pulte; Alasdair Armstrong; Jean Pichon-Pharabod; Luc Maranget; Peter Sewell (ESOP, 2020)

Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. - Alasdair Armstrong; Brian Campbell 001; Ben Simner; Christopher Pulte; Peter Sewell (CAV (1), 2021)

Relaxed virtual memory in Armv8-A. - Ben Simner; Alasdair Armstrong; Jean Pichon-Pharabod; Christopher Pulte; Richard Grisenthwaite; Peter Sewell (ESOP, 2022)

Relaxed virtual memory in Armv8-A (extended version). - Ben Simner; Alasdair Armstrong; Jean Pichon-Pharabod; Christopher Pulte; Richard Grisenthwaite; Peter Sewell (CoRR, 2022)

Wait-Free Weak Reference Counting. - Matthew J. Parkinson; Sylvan Clebsch; Ben Simner (ISMM, 2023)

Relaxed exception semantics for Arm-A (extended version). - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (CoRR, 2024)

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). - Alasdair Armstrong; Brian Campbell 001; Ben Simner; Christopher Pulte; Peter Sewell (Formal Methods Syst. Des., 2024)

Precise exceptions in relaxed architectures. - Ben Simner; Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Ohad Kammar; Jean Pichon-Pharabod; Peter Sewell (ISCA, 2025)