Formal models of ARM processors in HOL

Add to your list(s) Download to your calendar using vCal

• Mike Gordon (University of Cambridge)
• Tuesday 04 May 2010, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

Presenters: Mike Gordon and Anthony Fox / This is a rehearsal of our HCSS talk on May 11

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.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.