Alasdair Armstrong
alasdair.armstrong@brunel.ac.uk
Department of Computer Science
St John's Building
Brunel University London
Uxbridge, Middlesex
UB8 3PH, UK
I'm currently a research assistant at Brunel University working with Dr. Brijesh Dongol on verifying transactional memory algorithms. I recently completed my PhD at the University of Sheffield under the supervision of Dr. Georg Struth, working on algebraic formal methods and the relyguarantee method. My current research interests primarily lie in using formal methods to verify concurrent programs, in particular those using transactional memory, and the use of interactive and automated theorem proving technology in this area. I am also interested in the integration of automated theorem proving into interactive systems, and dependentlytyped functional programming.
Publications

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