Anthony Fox

Links

• The L3 specification language.
• A web-interface to the (old) ARM model.

Publications and reports

• 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. Formal verification of the ARM6 micro-architecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.
• Anthony Fox. A HOL specification of the ARM instruction set architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
• Anthony Fox. An algebraic framework for modelling and verifying microprocessors using HOL. Technical report No. 512, University of Cambridge Computer Laboratory, April 2001.
• Anthony Fox and Neal Harman. Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298-312, 2000.
• Anthony Fox. Algebraic Models for Advanced Microprocessors, PhD thesis, Swansea University, 1998.
• 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.

Other papers

• Verifying the ARM Block Data Transfer Instructions. Presented at DCC 2004.
• Verifying ARM6 Multiplication.