Formal Specification and Verification of ARM6
This page documents results of the University of Cambridge part of EPSRC project
The research was carried out by Anthony Fox.
The Principal Investigator was Mike Gordon.
Publications and Reports
- 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
- A.C.J. Fox and N.A. Harman,
Algebraic Models of Correctness for Microprocessors. Formal
Aspects of Computing, 12(4): 298-312, 2000.
Follow on research plans
Professor Mike Gordon
University of Cambridge
William Gates Building
JJ Thomson Avenue,
Cambridge CB3 0FD
work phone: +44 1223 334627
work fax: +44 1223 334678