BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Proof-producing decompilation and compilation - Magnus Myreen (Uni
 versity of Cambridge)
DTSTART:20080527T120000Z
DTEND:20080527T130000Z
UID:TALK11659@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Realistic formal specifications of machine languages for comme
 rcial processors consist of thousands of lines of definitions. Current met
 hods support formal proofs of the correctness of programs for one such spe
 cification. However\, these methods provide little or no support for reusi
 ng proofs of the same algorithm implemented in different machine languages
 .\n\nI'll describe an approach\, based on proof-producing decompilation\, 
 which both makes machine-code verification tractable and supports proof re
 use between different languages. With minor modifications a decompiler can
  be changed into compiler\, which plugs together verified\nprogram compone
 nts.
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR