BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal models of ARM processors in HOL - Mike Gordon (University o
 f Cambridge)
DTSTART:20100504T120000Z
DTEND:20100504T130000Z
UID:TALK24358@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The ARM verification project has produced a public domain mode
 l (formalised in higher order logic and mechanised in the HOL4 system) of 
 current ARM instruction set architectures. The model covers the machine co
 de semantics of both old (e.g. ARM7 from the 1990s) and brand new processo
 rs (Cortex-A8 and Cortex-A9) as found in phones and\nforthcoming netbooks.
  It is believed that this is one of the most complete and accurate formal 
 models of a COTS processor family in existence.\n\nTwo purposes of the ARM
  model are:\n\n(i) to provide a reference semantics for use in verifying s
 oftware running on ARM hardware\;<br/>\n(ii) to provide a research platfor
 m for gaining a deeper\nscientific understanding of areas whose mathematic
 al\npecification is challenging.<br/>\n\nAn example of (i) is the verifica
 tion (by Magnus Myreen) of a complete prototype functional language implem
 entation in ARM machine code\, including a garbage collector for memory ma
 nagement. Examples of (ii) include models of interrupts\, input-output and
  (in collaboration with Peter Sewell's group at Cambridge) mathematical fo
 rmalisations of ARM's weak memory model as used in multi-processor systems
 .\n\nIn 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 assu
 rance 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. \n\nWe would like to find new users of the AR
 M model and are willing to work with them to make it more suitable to thei
 r needs.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR