BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A tool for verification: A decompiler from ARM to HOL - Magnus Myr
 een (University of Cambridge)
DTSTART:20071030T130000Z
DTEND:20071030T140000Z
UID:TALK8507@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Magnus Myreen\n\nA year ago I presented a Hoare logic
  for machine code. The logic has since been used to verify a variety of pr
 ograms\, many with applications in elliptic curve cryptography but also a 
 small garbage collector.\n\nIn this talk I will present some automation th
 at was developed to ease the verification effort: a decompiler which given
  some ARM machine code produces a\nHOL function and proves that the ARM co
 de executes\nthe HOL function. Hence it performs the Hoare logic\nreasonin
 g for the user and leaves the user to concentrate\non proving properties o
 f fairly clean HOL functions\nrather than Hoare triples (or next-state fun
 ctions).
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR