BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:'Full Functional Verification of Linked Data Structures'\, Zee\, K
 uncak and Rinard - Viktor Vafeiadis (Microsoft Research Cambridge)
DTSTART:20091007T100000Z
DTEND:20091007T113000Z
UID:TALK19891@talks.cam.ac.uk
CONTACT:Mike Dodds
DESCRIPTION:This talk will cover two papers:\n\nFull Functional Verificati
 on of Linked Data Structures\n\nhttp://lara.epfl.ch/~kuncak/papers/ZeeETAL
 08FullFunctionalVerification\n\nAn Integrated Proof Language for Imperativ
 e Programs\n\nhttp://lara.epfl.ch/~kuncak/papers/ZeeETAL09IntegratedProofL
 anguageforImperativePrograms.pdf\n\n\nWe present the first verification of
  full functional correctness for a range of linked data structure implemen
 tations\, including mutable lists\, trees\, graphs\, and hash tables. Spec
 ifically\, we present the use of the Jahob verification system to verify f
 ormal specifications\, written in classical higher-order logic\, that comp
 letely capture the desired behavior of the Java data structure implementat
 ions (with the exception of properties involving execution time and/or mem
 ory consumption). Given that the desired correctness properties include in
 tractable constructs such as quantifiers\, transitive closure\, and lambda
  abstraction\, it is a challenge to successfully prove the generated verif
 ication conditions.\n\nOur Jahob verification system uses integrated reaso
 ning to split each verification condition into a conjunction of simpler su
 bformulas\, then apply a diverse collection of specialized decision proced
 ures\, first-order theorem provers\, and\, in the worst case\, interactive
  theorem provers to prove each subformula. Techniques such as replacing co
 mplex subformulas with stronger but simpler alterna- tives\, exploiting st
 ructure inherently present in the verification con- ditions\, and\, when n
 ecessary\, inserting verified lemmas and proof hints into the imperative s
 ource code make it possible to seamlessly integrate all of the specialized
  decision procedures and theorem provers into a single powerful integrated
  reasoning system. By appropriately applying multiple proof techniques to 
 discharge different subformulas\, this reasoning system can effectively pr
 ove the complex and challenging verification conditions that arise in this
  context.
LOCATION:FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR