PhD student in the Computer Science Department at the University of Cambridge.
angus.hammond at cl.cam.ac.uk
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
- Islaris, Coq formalisation and frontend tooling for machine code verification.
- 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 Jul 2022