Angus Hammond

PhD student in the Computer Science Department at the University of Cambridge.

Contact

angus.hammond at cl.cam.ac.uk

Research interests

I am interested in developing practical proof techniques for reasoning about realistic hardware systems, with a view to allowing low level program proof on CHERI processors.

Software

• Islaris, Coq formalisation and frontend tooling for machine code verification.
• AxSL, Coq formalisation of the AxSL program logic for the Arm weak memory model.

Publications

DBLP

• An axiomatic basis for computer programming on the relaxed Arm-A architecture: The AxSL logic, Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod, in POPL 2024 pdf
• Islaris: Verification of Machine Code Against Authoritative ISA Semantics, Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell, in PLDI 2022 pdf

Last modified: 26 Nov 2024