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 relyguarantee. My current research interests primarily lie in using formal methods to verify realworld programs, especially concurrent programs, and the use of interactive and automated theorem proving technology in this area. I'm also interested transactional memory and dependentlytyped functional programming.
Publications

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

B. Simner, A. Armstrong, J. PichonPharabod, C. Pulte, R. Grisenthwaite, P. Sewell. Relaxed virtual memory in Armv8A. 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 Capabilityenhanced Prototype Arm Architecture. ESOP 2022

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

B. Simner, S. Flur, C. Pulte, A. Armstrong, J. PichonPharabod, L. Maranget, P. Sewell. ARMv8A 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 ARMv8A, RISCV, and CHERIMIPS. POPL 2019
 B. Dongol, R. Jagadeesan, J. Riely, A. Armstrong. On abstraction and compositionality for weakmemory 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):265293 (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 RelyGuarantee 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 TarskiKleene hierarchy. In R. Berghammer, B. Möller and M. Winter (eds.), Journal of Logical and Algebraic Methods in Programming, 83(2):87102 (March 2014).

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

A. Armstrong and G. Struth. Automated Reasoning in HigherOrder 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 preprint 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 online 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