An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. - Kathryn E. Gray; Gabriel Kerneis; Dominic P. Mulligan; Christopher Pulte; Susmit Sarkar; Peter Sewell (MICRO, 2015)

Modelling the ARMv8 architecture, operationally: concurrency and ISA. - Shaked Flur; Kathryn E. Gray; Christopher Pulte; Susmit Sarkar; Ali Sezgin; Luc Maranget; Will Deacon; Peter Sewell (POPL, 2016)

Mixed-size concurrency: ARM, POWER, C/C++11, and SC. - Shaked Flur; Susmit Sarkar; Christopher Pulte; Kyndylan Nienhuis; Luc Maranget; Kathryn E. Gray; Ali Sezgin; Mark Batty; Peter Sewell (POPL, 2017)

Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. - Christopher Pulte; Shaked Flur; Will Deacon; Jon French; Susmit Sarkar; Peter Sewell (Proc. ACM Program. Lang., 2018)

Promising-ARM/RISC-V: a simpler and faster operational concurrency model. - Christopher Pulte; Jean Pichon-Pharabod; Jeehoon Kang; Sung-Hwan Lee 001; Chung-Kil Hur (PLDI, 2019)

ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. - Alasdair Armstrong; Thomas Bauereiss; Brian Campbell 001; Alastair Reid 001; Kathryn E. Gray; Robert M. Norton; Prashanth Mundkur; Mark Wassell; Jon French; Christopher Pulte; Shaked Flur; Ian Stark; et al. (Proc. ACM Program. Lang., 2019)

The semantics of multicopy atomic ARMv8 and RISC-V - Christopher Pulte (2019)

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)

Repairing and mechanising the JavaScript relaxed memory model. - Conrad Watt; Christopher Pulte; Anton Podkopaev; Guillaume Barbier; Stephen Dolan; Shaked Flur; Jean Pichon-Pharabod; Shu-yu Guo (PLDI, 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)

CN: Verifying Systems C Code with Separation-Logic Refinement Types. - Christopher Pulte; Dhruv C. Makwana; Thomas Sewell; Kayvan Memarian; Peter Sewell; Neel Krishnaswami (Proc. ACM Program. Lang., 2023)

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)

Fulminate: Testing CN Separation-Logic Specifications in C. - Rini Banerjee; Kayvan Memarian; Dhruv C. Makwana; Christopher Pulte; Neel Krishnaswami; Peter Sewell (Proc. ACM Program. Lang., 2025)