Alasdair Armstrong

Department of Computer Science
St John's Building
Brunel University London
Uxbridge, Middlesex

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.



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