Abstract

The ARM verification project has produced a public domain model (formalised in higher order logic and mechanised in the HOL4 system) of current ARM instruction set architectures. The model covers the machine code semantics of both old (e.g. ARM7 from the 1990s) and brand new processors (Cortex-A8 and Cortex-A9) as found in phones and forthcoming netbooks. It is believed that this is one of the most complete and accurate formal models of a COTS processor family in existence.

Two purposes of the ARM model are:

(i) to provide a reference semantics for use in verifying software running on ARM hardware;
(ii) to provide a research platform for gaining a deeper scientific understanding of areas whose mathematical pecification is challenging.

An example of (i) is the verification (by Magnus Myreen) of a complete prototype functional language implementation in ARM machine code, including a garbage collector for memory management. Examples of (ii) include models of interrupts, input-output and (in collaboration with Peter Sewell’s group at Cambridge) mathematical formalisations of ARM ’s weak memory model as used in multi-processor systems.

In the first part of the talk Mike Gordon will present an overview of the ARM project and how its results might be used for achieving high assurance software. The second part of the talk will be given by Anthony Fox, who will demonstrate the HOL model via an easy to use web interface that has recently been developed.

We would like to find new users of the ARM model and are willing to work with them to make it more suitable to their needs.