Publications
- Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew
Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell. Rigorous engineering for hardware security:
Formal modelling and proof
in the CHERI design and implementation process. IEEE Symposium on Security and Privacy 2020
- Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish. The
verified CakeML compiler backend. J. Funct. Program. 29 (2019)
- Jonathan Woodruff, Alexandre Joannou, Hongyan Xia, Anthony C. J. Fox, Robert M. Norton, David Chisnall, Brooks
Davis, Khilan Gudka, Nathaniel Wesley Filardo, A. Theodore Markettos, Michael Roe, Peter G. Neumann, Robert N. M.
Watson, Simon W. Moore. CHERI Concentrate: Practical
Compressed Capabilities. IEEE Trans. Computers 68(10) (2019)
- Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar
Abrahamsson, Anthony C. J. Fox. Verified compilation on a
verified processor. PLDI 2019
- Heiko Becker, Nikita Zyuzin, Raphael Monat, Eva Darulova, Magnus O. Myreen, Anthony Fox. A Verified Certificate Checker for Finite-Precision Error Bounds in Coq
and HOL4. FMCAD 2018
- Anthony Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar. Verified Compilation of
CakeML to Multiple Machine-Code Targets. CPP'17, 2017
- Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish. A New Verified Compiler Backend for CakeML.
ICFP'16, 2016
- Anthony Fox. Improved Tool Support for Machine-Code Decompilation in HOL4. In
Interactive Theorem Proving (ITP), 2015
- Anthony Fox. Directions in ISA specification. In Interactive Theorem Proving
(ITP), 2012
- Sascha Böhme, Anthony Fox, Thomas Sewell and Tjark Weber. Reconstruction of Z3's Bit-Vector Proofs in HOL4
and Isabelle/HOL. In First International Conference on Certified Programs and Proofs (CPP 2011)
- Anthony Fox. LCF-style Bit-Blasting
in HOL4. In Interactive Theorem Proving (ITP), 2011
- Anthony Fox and Magnus O. Myreen. A
Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving
(ITP), 2010
- Anthony Fox, Michael Gordon, and Magnus O. Myreen. Specification and verification
of ARM hardware and software. In David S. Hardin, editor, Design and
Verification of Microprocessor Systems for High-Assurance Applications, pages 221-248. Springer, 2010
- Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa
Nardelli. The Semantics of Power and ARM Multiprocessor
Machine Code. DAMP 09
- Magnus O. Myreen, Anthony Fox and Michael Gordon. Hoare Logic for ARM Machine Code. In
Fundamentals of Software Engineering (FSEN), 2007
- Anthony Fox. An algebraic framework for verifying the correctness of hardware with input and output: a
formalization in HOL. In J.L. Fiadeiro et al. (Eds.): CALCO 2005, LNCS 3629, pp. 157-174, 2005
- Anthony Fox and Neal Harman. Algebraic models of correctness for abstract pipelines. The Journal of Logic and
Algebraic Programming, 57(1-2): 71-107, 2003
- Anthony Fox. Formal specification and verification of ARM6. In David Basin and Burkhart Wolff, editors, TPHOLs
'03, volume 2758 of LNCS, pages 25-40. Springer-Verlag, 2003
- Anthony Fox and Neal Harman. Algebraic Models of Correctness for Microprocessors. Formal Aspects of
Computing, 12(4): 298-312, 2000
- Anthony Fox and Neal Harman. Algebraic Models of Superscalar Microprocessor Implementations: A Case Study.
Prospects for Hardware Foundations: 138-183, 1998
- Anthony Fox and Neal Harman. An Algebraic Model of Correctness for Superscalar Microprocessors. FMCAD: 346-361,
1996
Reports and Thesis
Other papers