Mathematizing C++ concurrency. - Mark Batty; Scott Owens; Susmit Sarkar; Peter Sewell; Tjark Weber (POPL, 2011)

Nitpicking C++ concurrency. - Jasmin Christian Blanchette; Tjark Weber; Mark Batty; Scott Owens; Susmit Sarkar (PPDP, 2011)

Synchronising C/C++ and POWER. - Susmit Sarkar; Kayvan Memarian; Scott Owens; Mark Batty; Peter Sewell; Luc Maranget; Jade Alglave; Derek Williams (PLDI, 2012)

Clarifying and compiling C/C++ concurrency: from C++11 to POWER. - Mark Batty; Kayvan Memarian; Scott Owens; Susmit Sarkar; Peter Sewell (POPL, 2012)

Library abstraction for C/C++ concurrency. - Mark Batty; Mike Dodds; Alexey Gotsman (POPL, 2013)

C/C++ Causal Cycles Confound Compositionality. - Mike Dodds; Mark Batty; Alexey Gotsman (Adv. Math. Commun., 2013)

GPU Concurrency: Weak Behaviours and Programming Assumptions. - Jade Alglave; Mark Batty; Alastair F. Donaldson; Ganesh Gopalakrishnan; Jeroen Ketema; Daniel Poetzl; Tyler Sorensen 001; John Wickerson (ASPLOS, 2015)

The Problem of Programming Language Concurrency Semantics. - Mark Batty; Kayvan Memarian; Kyndylan Nienhuis; Jean Pichon-Pharabod; Peter Sewell (ESOP, 2015)

Remote-scope promotion: clarified, rectified, and verified. - John Wickerson; Mark Batty; Bradford M. Beckmann; Alastair F. Donaldson (OOPSLA, 2015)

Taming the complexities of the C11 and OpenCL memory models. - John Wickerson; Mark Batty (CoRR, 2015)

The C11 and C++11 concurrency model. - Mark John Batty (2015)

Portable inter-workgroup barrier synchronisation for GPUs. - Tyler Sorensen 001; Alastair F. Donaldson; Mark Batty; Ganesh Gopalakrishnan; Zvonimir Rakamaric (OOPSLA, 2016)

Overhauling SC atomics in C11 and OpenCL. - Mark Batty; Alastair F. Donaldson; John Wickerson (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)

Automatically comparing memory consistency models. - John Wickerson; Mark Batty; Tyler Sorensen 001; George A. Constantinides (POPL, 2017)

Compositional Verification of Compiler Optimisations on Relaxed Memory. - Mike Dodds; Mark Batty; Alexey Gotsman (ESOP, 2018)

PrideMM: Second Order Model Checking for Memory Consistency Models. - Simon Cooksey; Sarah Harris; Mark Batty; Radu Grigore; Mikolás Janota (FM Workshops (2), 2019)

PrideMM: A Solver for Relaxed Memory Models. - Simon Cooksey; Sarah Harris; Mark Batty; Radu Grigore; Mikolás Janota (CoRR, 2019)

Modular Relaxed Dependencies in Weak Memory Concurrency. - Marco Paviotti; Simon Cooksey; Anouk Paradis; Daniel Wright 001; Scott Owens; Mark Batty (ESOP, 2020)

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies. - Daniel Wright 001; Mark Batty; Brijesh Dongol (FM, 2021)

Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version). - Daniel Wright 001; Mark Batty; Brijesh Dongol (CoRR, 2021)

Chronos vs. Chaos: Timing Weak Memory Executions in the Linux Kernel. - Sam Dawson; Mark Batty (IWSPA@CODASPY, 2022)

The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency. - Alan Jeffrey; James Riely; Mark Batty; Simon Cooksey; Ilya Kaysin; Anton Podkopaev (Proc. ACM Program. Lang., 2022)

Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Experience Paper). - Sarah Harris; Simon Cooksey; Michael Vollmer 003; Mark Batty (ECOOP, 2023)

Memory Consistency Models for Program Transformations: An Intellectual Abstract. - Akshay Gopalakrishnan; Clark Verbrugge; Mark Batty (ISMM, 2023)

Verifying Read-Copy Update Under RC11. - Mikhail Semenyuk; Mark Batty; Brijesh Dongol (SEFM, 2023)

Rust for Morello: Always-On Memory Safety, Even in Unsafe Code (Artifact). - Sarah Harris; Simon Cooksey; Michael Vollmer 003; Mark Batty (Dagstuhl Artifacts Ser., 2023)

Mechanised Operational Reasoning for C11 Programs with Relaxed Dependencies. - Daniel Wright 001; Sadegh Dalvandi; Mark Batty; Brijesh Dongol (Formal Aspects Comput., 2023)

Memory Consistency and Program Transformations. - Akshay Gopalakrishnan; Clark Verbrugge; Mark Batty (CoRR, 2024)

Spegion: Implicit and Non-Lexical Regions with Sized Allocations. - Jack Hughes 002; Michael Vollmer 003; Mark Batty (ECOOP, 2025)

Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice. - Jay Richards; Daniel Wright 001; Simon Cooksey; Mark Batty (Proc. ACM Program. Lang., 2025)