About me

Automated Reasoning Group, Amazon Web Services 2022–present

I am a Principal Applied Scientist within the Automated Reasoning Group at Amazon Web Services, Cambridge. I work on the verification of correctness and security properties of ultra low-level code.

Systems Research Group, Arm Research 2017–2022

I was (eventually promoted to become a) Principal Research Engineer within the Systems Group at Arm Research, Cambridge. My research at Arm focussed on privacy-preserving computation, as evidenced by the Confidential Computing Consortium-adopted Veracruz project, a project which I initiated and thereafter acted as technical lead on.

I also helped develop software verification flows which provided strong evidence for the correctness for low-level, security-critical firmware, central to the Arm Confidential Computing Architecture, or Arm CCA. This is a Confidential Computing technology that will be deployed as a point-release for the Armv9-A architecture and will eventually be found in hundreds of millions of devices worldwide.

Computer Laboratory, University of Cambridge 2012–2017

I was a Postdoctoral Research Scientist at the Computer Laboratory at the University of Cambridge. Here, I worked on Prof. Peter Sewell’s Rigorous Engineering for Mainstream Systems project, or REMS.

At Cambridge I helped design and develop the Lem specification language, and thereafter used Lem to formally specify the semantics of ELF static linking. I also developed a side interest in the correctness of a class of distributed datastructure, called Conflict-free Replicated Datatypes, or CRDTs.

Dipartimento di Scienze dell'Informazione, University of Bologna, Italy 2010–2012

I was a Postdoctoral Research Scientist at the Dipartimento di Scienze dell’Informazione at the Alma Mater Studiorum, Università di Bologna. I worked with Dr. Claudio Sacerdoti Coen on the EU-funded Certified Complexity project, or CerCo.

CerCo aimed to produce a certified compiler, for a large fragment of C, capable of automatically lifting precise and reliable concrete complexity bounds from machine code to the original input source code. I worked on the implementation and verification of the CerCo C compiler backend, using the now sadly defunct Matita proof assistant.

Heriot-Watt University, Edinburgh 2007–2010

I obtained my PhD in theoretical computer science from the Department of Mathematics and Computer Science at Heriot-Watt University, Edinburgh. I studied various topics at the intersection of nominal techniques, unification, and type-theory and lambda-calculi. My supervisors were Dr. Murdoch “Jamie” Gabbay and Prof. Phil Trinder.

Whilst a PhD student I used to play rugby union — starting in the backs, before ending up playing as a loosehead prop in the front row — for Lismore RUFC. In summer, I also played cricket for Woodcutters Cricket Club.

University of Edinburgh 2003–2007

I graduated with a first-class honours degree in Artificial Intelligence and Computer Science from the Department of Informatics at the University of Edinburgh.