Anthony Fox

Links

• ARM in HOL.

Publications and reports

• 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 C. J. Fox. LCF-style Bit-Blasting in HOL4. In Interactive Theorem Proving (ITP), 2011.
• Anthony C. J. Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), 2010.
• Anthony C. J. Fox, Michael J. C. 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 C. J. Fox and Michael J. C. Gordon. Hoare Logic for ARM Machine Code. In Fundamentals of Software Engineering (FSEN), 2007.
• A.C.J 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.
• A.C.J Fox and N.A. Harman. Algebraic models of correctness for abstract pipelines. The Journal of Logic and Algebraic Programming, 57(1-2): 71-107, 2003.
• A.C.J 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.
• A.C.J. Fox. Formal verification of the ARM6 micro-architecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.
• A.C.J. Fox. A HOL specification of the ARM instruction set architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
• A.C.J. Fox. An algebraic framework for modelling and verifying microprocessors using HOL. Technical report No. 512, University of Cambridge Computer Laboratory, April 2001.
• A.C.J. Fox and N.A. Harman. Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298-312, 2000.
• A.C.J. Fox. Algebraic Models for Advanced Microprocessors, PhD thesis, Swansea University, 1998.

Other papers

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