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. I completed my PhD at the University of Sheffield under the supervision of Dr. Georg Struth, working on algebraic formal methods and rely-guarantee. My current research interests primarily lie in using formal methods to verify real-world programs, especially concurrent programs, and the use of interactive and automated theorem proving technology in this area. I'm also interested transactional memory and dependently-typed functional programming.

Publications

• 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 (2023)

• 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