BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compositional Inter-Language Relational Verification - Chung-Kil H
 ur\, Max Planck Institute for Software Systems
DTSTART:20120330T090000Z
DTEND:20120330T100000Z
UID:TALK37088@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The "relational" approach to program verification involves sho
 wing that some lower-level program of interest is equivalent to (or a refi
 nement of) some higher-level program\, which may in turn prove more amenab
 le to traditional verification techniques.  Thanks to recent advances in t
 heorem proving technology\, the relational approach has been shown to scal
 e to the verification of significant software systems\, such as seL4 and t
 he certified CompCert compiler for C.\n\nHowever\, existing relational met
 hods apply only to the verification of *whole* software systems.  For inst
 ance\, the correctness of the CompCert compiler is guaranteed only when it
  is used to compile whole programs\, since the underlying proof method lac
 ks *compositionality*.\n\nInformally\, compositionality means that the ver
 ification of a whole program may be obtained by composing together the ver
 ification of its modular subcomponents.\n\nIn this talk\, I will present t
 wo notions of compositionality arising in relational verification -- horiz
 ontal and vertical compositionality-- and discuss the extent to which exis
 ting relational techniques do or do not support them.  I will then discuss
  my own work toward fully compositional inter-language relational verifica
 tion\, in particular: (1) the development of a compositional\, *semantic* 
 notion of equivalence between high- and low-level languages\, and (2) the 
 invention of a novel relational technique\, *parametric bisimulations*\, w
 hich supports both horizontal and vertical notions of compositionality.\n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR