BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified just-in-time compiler on x86 - Magnus Myreen (University 
 of Cambridge)
DTSTART:20091215T130000Z
DTEND:20091215T140000Z
UID:TALK19688@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:(An 18-minute practice talk for POPL 2010.)\n\nThis paper pres
 ents a method for creating formally correct just-in-time (JIT) compilers. 
 The tractability of our approach is demonstrated through\, what we believe
  is the first\, verification of a JIT compiler with respect to a realistic
  semantics of self-modifying x86 machine code. Our semantics includes a mo
 del of the instruction\ncache. Two versions of the verified JIT compiler a
 re presented: one generates all of the machine code at once\, the other on
 e is incremental i.e. produces code on-demand. All proofs have been perfor
 med inside the HOL4 theorem prover.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR