Anthony C. J. Fox

According to our database, Anthony C. J. Fox authored at least 26 papers between 1996 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

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., April, 2023

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

Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.

Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

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

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2020

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, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

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, Robert N. M. Watson, Simon W. Moore

IEEE Trans. Computers, 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

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

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018

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

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

2017

Verified compilation of CakeML to multiple machine-code targets.

Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar

Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017

2016

A new verified compiler backend for CakeML.

Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

2015

Improved Tool Support for Machine-Code Decompilation in HOL4.

Anthony C. J. Fox

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2012

Directions in ISA Specification.

Anthony C. J. Fox

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

LCF-Style Bit-Blasting in HOL4.

Anthony C. J. Fox

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.

Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.

Anthony C. J. Fox, Magnus O. Myreen

Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Specification and Verification of ARM Hardware and Software.

Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

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

Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, 2009

2007

Hoare Logic for ARM Machine Code.

Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon

Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007

2005

An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL.

Anthony C. J. Fox

Proceedings of the Algebra and Coalgebra in Computer Science: First International Conference, 2005

2003

Algebraic models of correctness for abstract pipelines.

Anthony C. J. Fox, Neal A. Harman

J. Log. Algebraic Methods Program., 2003

Formal Specification and Verification of ARM6.

Anthony C. J. Fox

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

2000

Algebraic Models of Correctness for Microprocessors.

Anthony C. J. Fox, Neal A. Harman

Formal Aspects Comput., 2000

1999

Algebraic models for advanced microprocessors.

Anthony C. J. Fox

PhD thesis, 1999

1998

Algebraic Models of Superscalar Microprocessor Implementations: A Case Study.

Anthony C. J. Fox, Neal A. Harman

Proceedings of the Prospects for Hardware Foundations, ESPRIT Working Group 8533, NADA, 1998

1996

An Algebraic Model of Correctness for Superscalar Microprocessors.

Anthony C. J. Fox, Neal A. Harman

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996