Automated Reasoning in Higher-Order Regular Algebra. - Alasdair Armstrong; Georg Struth (RAMiCS, 2012)

Dependently Typed Programming Based on Automated Theorem Proving. - Alasdair Armstrong; Simon Foster 001; Georg Struth (MPC, 2012)

Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. - Alasdair Armstrong; Georg Struth; Tjark Weber (ITP, 2013)

Kleene Algebra. - Alasdair Armstrong; Georg Struth; Tjark Weber (Arch. Formal Proofs, 2013)

Algebras for Program Correctness in Isabelle/HOL. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (RAMiCS, 2014)

Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (FM, 2014)

Lightweight Program Construction and Verification Tools in Isabelle/HOL. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (SEFM, 2014)

Kleene Algebra with Tests and Demonic Refinement Algebras. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (Arch. Formal Proofs, 2014)

Programming and automating mathematics in the Tarski-Kleene hierarchy. - Alasdair Armstrong; Georg Struth; Tjark Weber (J. Log. Algebraic Methods Program., 2014)

Formal analysis of concurrent programs. - Alasdair Armstrong (2015)

Reducing Opacity to Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (CoRR, 2016)

Building program construction and verification tools from algebraic principles. - Alasdair Armstrong; Victor B. F. Gomes; Georg Struth (Formal Aspects Comput., 2016)

Modularising Opacity Verification for Hybrid Transactional Memory. - Alasdair Armstrong; Brijesh Dongol (FORTE, 2017)

Proving Opacity via Linearizability: A Sound and Complete Method. - Alasdair Armstrong; Brijesh Dongol; Simon Doherty (FORTE, 2017)

On abstraction and compositionality for weak-memory linearisability. - Brijesh Dongol; Radha Jagadeesan; James Riely; Alasdair Armstrong (VMCAI, 2018)

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)

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)

Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. - Thomas Bauereiss; Brian Campbell 001; Thomas Sewell; Alasdair Armstrong; Lawrence Esswood; Ian Stark; Graeme Barnes; Robert N. M. Watson; Peter Sewell (ESOP, 2022)

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)

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)

Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor. - Louis-Emile Ploix; Alasdair Armstrong; Tom Melham; Ray Lin; Haolong Wang; Anastasia Courtney (CoRR, 2025)