Alasdair Armstrong

alasdair.armstrong@cl.cam.ac.uk

Computer Laboratory
University of Cambridge
JJ Thomson Avenue
Cambridge
CB3 0FD, UK

I'm currently a research assistant at Cambridge University working with Prof. Peter Sewell on the REMS project. My research focuses on large-scale semantics for instruction set architecture (ISA) definitions. ISAs represent the contract between hardware and software, as used by software like operating systems, hypervisors, and compilers.

I previously completed my PhD at the University of Sheffield under the supervision of Dr. Georg Struth, working on algebraic formal methods and rely-guarantee. I've also worked on transactional memory, verifying in Isabelle/HOL hybrid transactional memory algorithms that mix hardware and software transactions, as well as specifying correctness conditions for transactions with relaxed memory concurrency.

Sail

Much of my research on ISA specifications focuses on the Sail language and Isla tool for relaxed concurrency. Sail is a domain-specific language for specifying ISAs that combines an intentionally simple semantics, with lightweight dependent types for bitvector widths to enable safely writing specifications that are extremely configurable and often very polymorphic over such bitvector widths. Isla allows symbolically executing Sail specifications, computing all possible allowed behaviours, which can then be combined with an arbitrary axiomatic concurrency model to evaluate concurrency litmus tests that use any architectural feature defined in Sail.

Sail is used for the RISC-V golden model, now developed within RISC-V international. It's also highly compatible with Arm's ASL language, which enabled our work on verifying capability secuirity properties as part of the UKRI funded Morello program.

Publications

• T. Pérami, T. Bauereiss, B. Campbell, Z. Liu, N. Lauermann, A. Armstrong, P. Sewell. ArchSem: Reusable Rigorous Semantics of Relaxed Architectures. POPL 2026

• B. Simner, A. Armstrong, T. Bauereiss, B. Campbell, O. Kammar, J. Pichon-Pharabod, P. Sewell. Precise exceptions in relaxed architectures. ISCA 2025

• L. Ploix, A. Armstrong, T. Melham, R. Lin, H. Wang, A. Courtney. Comprehensive Formal Verification of Observational Correctness for the CHERIoT-Ibex Processor.

  Preprint is available on arXiv here

• A. Armstrong, B. Campbell, B. Simner, C. Pulte, P. Sewell. Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models (extended version). Formal Methods in System Design (2024)

• B. Simner, A. Armstrong, J. Pichon-Pharabod, C. Pulte, R. Grisenthwaite, P. Sewell. Relaxed virtual memory in Armv8-A. ESOP 2022

• T. Bauereiss, B. Campbell, T. Sewell, A. Armstrong, L. Esswood, I. Stark, G. Barnes, R. N. M. Watson, P. Sewell. Verified Security for the Morello Capability-enhanced Prototype Arm Architecture. ESOP 2022

• A. Armstrong, B. Campbell, B. Simner, C. Pulte, P. Sewell. Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models. CAV 2021

• B. Simner, S. Flur, C. Pulte, A. Armstrong, J. Pichon-Pharabod, L. Maranget, P. Sewell. ARMv8-A system semantics: Instruction fetch in relaxed architectures. ESOP 2020

• A. Armstrong, T. Bauereiss, B. Campbell, A. Reid, K. E. Gray, R. M. Norton, P. Mundkur, M. Wassell, J. French, C. Pulte, S. Flur, I. Stark, N. Krishnaswami, P. Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. POPL 2019

• B. Dongol, R. Jagadeesan, J. Riely, A. Armstrong. On abstraction and compositionality for weak-memory linearisability. VMCAI 2018

• A. Armstrong, B. Dongol. Modularising opacity verification for hybrid transactional memory. FORTE 2017, (June 2017)

• A. Armstrong, B. Dongol, S. Doherty. Proving opacity via linearizability: A sound and complete method. FORTE 2017, (June 2017)

• A. Armstrong, V. B. F. Gomes and G. Struth. Building program construction and verification tools from algebraic principles. Formal Aspects of Computing, 28(2):265-293 (April 2016)

• A. Armstrong, V. B. F. Gomes and G. Struth. Lightweight Program Construction and Verification Tools in Isabelle/HOL. In D. Giannakopoulou and G. Salaün (eds.), SEFM 2014, LNCS 8702.

• A. Armstrong, V. B. F. Gomes and G. Struth. Algebras for program correctness in Isabelle/HOL. In P. Höfner, P. Jipsen, W. Kahl and M. E. Müller (eds.), RAMiCs 2014, LNCS 8428.

• A. Armstrong, V. B. F. Gomes and G. Struth. Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools. In C. Jones, P. Pihlajasaari and J. Sun (eds.), FM 2014, LNCS 8442.

• A. Armstrong, G. Struth and T. Weber. Programming and automating mathematics in the Tarski-Kleene hierarchy. In R. Berghammer, B. Möller and M. Winter (eds.), Journal of Logical and Algebraic Methods in Programming, 83(2):87-102 (March 2014).

• A. Armstrong, G. Struth and T. Weber. Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL. In S. Blazy, C. Paulin-Mohring and D. Pichardie (eds.), ITP 2013, LNCS 7998.

• A. Armstrong and G. Struth. Automated Reasoning in Higher-Order Regular Algebra. In T. Griffin and W. Kahl (eds.), RAMiCS 2012, LNCS 7560.

  Our Isabelle theory file which accompanies the paper can be found here.

• A. Armstrong, S. Foster and G. Struth. Dependently Typed Programming based on Automated Theorem Proving. In J. Gibbons and P. Nogueira (eds.), MPC 2012, LNCS 7342.

  A pre-print with more details of the Haskell implementation is available on arXiv. Source code can be found here.

• P. Quinn, D. Rout, L. Stringer, T. Alexander, A. Armstrong and S. Olmstead. Petrodatabase: an on-line database for thin section ceramic petrography. Journal of Archaeological Science, Volume 38, Issue 9, September 2011.

Thesis

My thesis is available online at the White Rose eThesis repository here.

Associated Isabelle theory files may be found on my github page.

Archive of Formal Proofs

• A. Armstrong, G. Struth and T. Weber. Kleene Algebra

• A. Armstrong, V. B. F. Gomes and G. Struth. Kleene Algebra with Tests and Demonic Refinement Algebras