BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Verified Bignum Implementation in x86-64 Machine Code - Magnus M
 yreen (University of Cambridge)
DTSTART:20131119T130000Z
DTEND:20131119T140000Z
UID:TALK48369@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:This is a 20-minute preview of a talk I'll give at CPP'13.\n\n
 Verification of machine code can easily deteriorate into an endless\nclutt
 er of low-level details. This paper presents a case study which\nshows tha
 t machine-code verification does not necessitate ghastly\nlow-level proofs
 .  The case study we describe is the construction of\nan x86-64 implementa
 tion of arbitrary-precision integer\narithmetic. Compared with closely rel
 ated work\, our proofs are shorter and\, more importantly\, the reasoning 
 is at a more convenient high level of abstraction\, e.g. pointer reasoning
  is largely avoided. We achieve this improvement as a result of using an a
 bstraction for arrays and previously developed tools\, namely\, a proof-pr
 oducing decompiler and compiler. The work presented in this paper has been
  developed in the HOL4 theorem prover. The case study resulted in 800 line
 s of verified 64-bit x86 machine code.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR