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)

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)

Armed Cats: Formal Concurrency Modelling at Arm. - Jade Alglave; Will Deacon; Richard Grisenthwaite; Antoine Hacquard; Luc Maranget (ACM Trans. Program. Lang. Syst., 2021)