Department of Computer Science
St John's Building
Brunel University London
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 rely-guarantee 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 dependently-typed functional programming.
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.
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.
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