An Algebraic Model of Correctness for Superscalar Microprocessors. - Anthony C. J. Fox; Neal A. Harman (FMCAD, 1996)

Algebraic Models of Superscalar Microprocessor Implementations: A Case Study. - Anthony C. J. Fox; Neal A. Harman (Prospects for Hardware Foundations, 1998)

Algebraic models for advanced microprocessors. - Anthony C. J. Fox (1999)

Algebraic Models of Correctness for Microprocessors. - Anthony C. J. Fox; Neal A. Harman (Formal Aspects Comput., 2000)

Formal Specification and Verification of ARM6. - Anthony C. J. Fox (TPHOLs, 2003)

Algebraic models of correctness for abstract pipelines. - Anthony C. J. Fox; Neal A. Harman (J. Log. Algebraic Methods Program., 2003)

An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL. - Anthony C. J. Fox (CALCO, 2005)

Hoare Logic for ARM Machine Code. - Magnus O. Myreen; Anthony C. J. Fox; Michael J. C. Gordon (FSEN, 2007)

The semantics of power and ARM multiprocessor machine code. - Jade Alglave; Anthony C. J. Fox; Samin Ishtiaq; Magnus O. Myreen; Susmit Sarkar; Peter Sewell; Francesco Zappa Nardelli (DAMP, 2009)

Specification and Verification of ARM Hardware and Software. - Anthony C. J. Fox; Michael J. C. Gordon; Magnus O. Myreen (Design and Verification of Microprocessor Systems for High-Assurance Applications, 2010)

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. - Anthony C. J. Fox; Magnus O. Myreen (ITP, 2010)

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. - Sascha Böhme; Anthony C. J. Fox; Thomas Sewell; Tjark Weber (CPP, 2011)

LCF-Style Bit-Blasting in HOL4. - Anthony C. J. Fox (ITP, 2011)

Directions in ISA Specification. - Anthony C. J. Fox (ITP, 2012)

Improved Tool Support for Machine-Code Decompilation in HOL4. - Anthony C. J. Fox (ITP, 2015)

A new verified compiler backend for CakeML. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (ICFP, 2016)

Verified compilation of CakeML to multiple machine-code targets. - Anthony C. J. Fox; Magnus O. Myreen; Yong Kiam Tan; Ramana Kumar (CPP, 2017)

A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. - Heiko Becker; Nikita Zyuzin; Raphaël Monat; Eva Darulova; Magnus O. Myreen; Anthony C. J. Fox (FMCAD, 2018)

Verified compilation on a verified processor. - Andreas Lööw; Ramana Kumar; Yong Kiam Tan; Magnus O. Myreen; Michael Norrish; Oskar Abrahamsson; Anthony C. J. Fox (PLDI, 2019)

The verified CakeML compiler backend. - Yong Kiam Tan; Magnus O. Myreen; Ramana Kumar; Anthony C. J. Fox; Scott Owens; Michael Norrish (J. Funct. Program., 2019)

CHERI Concentrate: Practical Compressed Capabilities. - 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; et al. (IEEE Trans. Computers, 2019)

Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. - Kyndylan Nienhuis; Alexandre Joannou; Thomas Bauereiss; Anthony C. J. Fox; Michael Roe; Brian Campbell 001; Matthew Naylor; Robert M. Norton; Simon W. Moore; Peter G. Neumann; Ian Stark; Robert N. M. Watson; et al. (SP, 2020)

Verified Compilation and Optimization of Floating-Point Programs in CakeML. - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (ECOOP, 2022)

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification. - Hrutvik Kanabar; Anthony C. J. Fox; Magnus O. Myreen (ITP, 2022)

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact). - Heiko Becker; Robert Rabe; Eva Darulova; Magnus O. Myreen; Zachary Tatlock; Ramana Kumar; Yong Kiam Tan; Anthony C. J. Fox (Dagstuhl Artifacts Ser., 2022)

A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. - Anthony C. J. Fox; Gareth Stockwell; Shale Xiong; Hanno Becker; Dominic P. Mulligan; Gustavo Petri; Nathan Chong (Proc. ACM Program. Lang., 2023)