BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic Reverse Engineering for Formal Verification - Magnus Myr
 een (University of Cambridge)
DTSTART:20090512T120000Z
DTEND:20090512T130000Z
UID:TALK17987@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:This is a practice talk for HCSS with not much new material.\n
 \nWe describe a novel method for machine-code verification: code is decomp
 iled into tail-recursive functions and then verification proofs are perfor
 med in the native language of a theorem prover. Unlike\nestablished method
 s\, our completely automatic decompiler allows proof reuse even between di
 fferent instruction architectures. As a case study\, we have verified full
  functional correctness of ARM\, x86 and PowerPC implementations of a vers
 ion of LISP similar to LISP 1.5. Our tools are implemented in the HOL4 sys
 tem.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR