Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Homepage: Anthony Fox

Anthony Fox

Research Associate.

University of Cambridge

Computer Laboratory

William Gates Building

15 JJ Thomson Avenue

Cambridge, CB3 0FD

Telephone: +44 (0)1223 763598

Publications and reports

Anthony C. J. Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. To appear 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 Applicaions, 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, University of Wales Swansea, 1998.

Publications before 1998

Unpublished papers

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