Anthony C. J. Fox

26 papers A* 2A 2B 10Journal 6Unranked 4
YearRankTypeTitle / Venue / Authors
2023 J jnl
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations.
Proc. ACM Program. Lang.
Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri, Nathan Chong
2022 B conf
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification.
ITP
Hrutvik Kanabar, Anthony C. J. Fox, Magnus O. Myreen
2022 J jnl
Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact).
Dagstuhl Artifacts Ser.
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2022 A conf
Verified Compilation and Optimization of Floating-Point Programs in CakeML.
ECOOP
Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, Anthony C. J. Fox
2020 A* conf
Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process.
SP
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
2019 J jnl
CHERI Concentrate: Practical Compressed Capabilities.
IEEE Trans. Computers
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
2019 J jnl
The verified CakeML compiler backend.
J. Funct. Program.
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
2019 A* conf
Verified compilation on a verified processor.
PLDI
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, Anthony C. J. Fox
2018 B conf
A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4.
FMCAD
Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, Anthony C. J. Fox
2017 B conf
Verified compilation of CakeML to multiple machine-code targets.
CPP
Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar
2016 A conf
A new verified compiler backend for CakeML.
ICFP
Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony C. J. Fox, Scott Owens, Michael Norrish
2015 B conf
Improved Tool Support for Machine-Code Decompilation in HOL4.
ITP
Anthony C. J. Fox
2012 B conf
Directions in ISA Specification.
ITP
Anthony C. J. Fox
2011 B conf
LCF-Style Bit-Blasting in HOL4.
ITP
Anthony C. J. Fox
2011 B conf
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL.
CPP
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber
2010 B conf
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture.
ITP
Anthony C. J. Fox, Magnus O. Myreen
2010 — ch.
Specification and Verification of ARM Hardware and Software.
Design and Verification of Microprocessor Systems for High-Assurance Applications
Anthony C. J. Fox, Michael J. C. Gordon, Magnus O. Myreen
2009 — conf
The semantics of power and ARM multiprocessor machine code.
DAMP
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli
2007 — conf
Hoare Logic for ARM Machine Code.
FSEN
Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon
2005 B conf
An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL.
CALCO
Anthony C. J. Fox
2003 J jnl
Algebraic models of correctness for abstract pipelines.
J. Log. Algebraic Methods Program.
Anthony C. J. Fox, Neal A. Harman
2003 — conf
Formal Specification and Verification of ARM6.
TPHOLs
Anthony C. J. Fox
2000 J jnl
Algebraic Models of Correctness for Microprocessors.
Formal Aspects Comput.
Anthony C. J. Fox, Neal A. Harman
1999 — —
Algebraic models for advanced microprocessors.
Anthony C. J. Fox
1998 — conf
Algebraic Models of Superscalar Microprocessor Implementations: A Case Study.
Prospects for Hardware Foundations
Anthony C. J. Fox, Neal A. Harman
1996 B conf
An Algebraic Model of Correctness for Superscalar Microprocessors.
FMCAD
Anthony C. J. Fox, Neal A. Harman