BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:High-Level Separation Logic for Low-Level Code - Nick Benton\, MSR
  Cambridge
DTSTART:20121210T130000Z
DTEND:20121210T140000Z
UID:TALK41248@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:(joint work with Jonas Jensen and Andrew Kennedy)\n\nSeparatio
 n logic is a powerful tool for reasoning about structured\, imperative pro
 grams that manipulate pointers. However\, its application to unstructured\
 , lower-level languages such as assembly language or machine code remains 
 challenging. We describe a separation logic tailored for this purpose that
  we have applied to x86 machine code programs.\n\nThe logic is built from 
 an assertion logic on machine states over which we construct a specificati
 on logic that encapsulates uses of frames and step indexing. The tradition
 al notion of Hoare triple is not applicable directly to unstructured machi
 ne code\, where code and data are mixed together and programs do not in ge
 neral run to completion\, so instead we adopt a continuation-passing style
  of specification with preconditions alone. Nevertheless\, the range of pr
 imitives provided by the specification logic\, which include a higher-orde
 r frame connective\, a novel read-only frame connective\, and a ‘later
 ’ modality\, support the definition of derived forms to support basic-bl
 ock-style reasoning for common cases\, in which standard rules for Hoare t
 riples are derived as lemmas. Furthermore\, our encoding of assembly langu
 age labels in terms of the more primitive code pointers lets us encapsulat
 e local usage of labels and the definition and rules for assembly-language
  ‘macros’ such as while loops and conditionals.\n\nWe have applied the
  framework to a model of x86 machine code built entirely within the Coq pr
 oof assistant\, including tactic support based on computational reflection
 .\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR