Anthony C. J. Fox

ORCID

Publication Activity (10 Years)

Years Active: 1996-2023
Publications (10 Years): 12

Top Venues

ITP

Proc. ACM Program. Lang.

IEEE Symposium on Security and Privacy

J. Funct. Program.

Swansea University, UK (PHD)

Education History

Swansea University, UK

PHD

Publications

Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML. ECOOP (2022)
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). Dagstuhl Artifacts Ser. 8 (2) (2022)
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. ITP (2022)
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)
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)
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)
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, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. FMCAD (2018)
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets. CPP (2017)
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
A new verified compiler backend for CakeML. ICFP (2016)
Anthony C. J. Fox
Improved Tool Support for Machine-Code Decompilation in HOL4. ITP (2015)
Anthony C. J. Fox
Directions in ISA Specification. ITP (2012)
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. CPP (2011)
Anthony C. J. Fox
LCF-Style Bit-Blasting in HOL4. ITP (2011)
Anthony C. J. Fox, Magnus O. Myreen
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. ITP (2010)
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
The semantics of power and ARM multiprocessor machine code. DAMP (2009)
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
Hoare Logic for ARM Machine Code. FSEN (2007)
Anthony C. J. Fox
An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL. CALCO (2005)
Anthony C. J. Fox
Formal Specification and Verification of ARM6. TPHOLs (2003)
Anthony C. J. Fox, Neal A. Harman
Algebraic models of correctness for abstract pipelines. J. Log. Algebraic Methods Program. 57 (1-2) (2003)
Anthony C. J. Fox, Neal A. Harman
Algebraic Models of Correctness for Microprocessors. Formal Aspects Comput. 12 (4) (2000)
Anthony C. J. Fox, Neal A. Harman
Algebraic Models of Superscalar Microprocessor Implementations: A Case Study. Prospects for Hardware Foundations (1998)
Anthony C. J. Fox, Neal A. Harman
An Algebraic Model of Correctness for Superscalar Microprocessors. FMCAD (1996)

Anthony C. J. Fox.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Anthony C. J. Fox