Formal Specification and Verification of ARM6

Final Report

Publications and Reports

1. 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.
2. 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.
3. A.C.J. Fox, Formal verification of the ARM6 micro-architecture. Technical report No. 548, University of Cambridge Computer Laboratory, November 2002.
4. A.C.J. Fox, A HOL specification of the ARM instruction set architecture. Technical report No. 545, University of Cambridge Computer Laboratory, June 2001.
5. 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.
6. A.C.J. Fox and N.A. Harman, Algebraic Models of Correctness for Microprocessors. Formal Aspects of Computing, 12(4): 298-312, 2000.

Unpublished papers

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

Other outputs

• A poster made midway through the project for the Official Opening of the William Gates Building.
• Online source files for the proofs done by Anthony Fox (kindly hosted by SourceForge.net Open Source software development website).

Follow on research plans

• Description of the proposed research for a follow-on project (funding decision awaited).
• Letter of support from ARM (discusses both the completed project and the proposed new one).