BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Program verification reading group.
SUMMARY:'Full Functional Verification of Linked Data Struc
tures'\, Zee\, Kuncak and Rinard - Viktor Vafeiadi
s (Microsoft Research Cambridge)
DTSTART;TZID=Europe/London:20091007T110000
DTEND;TZID=Europe/London:20091007T123000
UID:TALK19891AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/19891
DESCRIPTION:This talk will cover two papers:\n\nFull Functiona
l Verification of Linked Data Structures\n\nhttp:/
/lara.epfl.ch/~kuncak/papers/ZeeETAL08FullFunction
alVerification\n\nAn Integrated Proof Language for
Imperative Programs\n\nhttp://lara.epfl.ch/~kunca
k/papers/ZeeETAL09IntegratedProofLanguageforImpera
tivePrograms.pdf\n\n\nWe present the first verific
ation of full functional correctness for a range o
f linked data structure implementations\, includin
g mutable lists\, trees\, graphs\, and hash tables
. Specifically\, we present the use of the Jahob v
erification system to verify formal specifications
\, written in classical higher-order logic\, that
completely capture the desired behavior of the Jav
a data structure implementations (with the excepti
on of properties involving execution time and/or m
emory consumption). Given that the desired correct
ness properties include intractable constructs suc
h as quantifiers\, transitive closure\, and lambda
abstraction\, it is a challenge to successfully p
rove the generated verification conditions.\n\nOur
Jahob verification system uses integrated reasoni
ng to split each verification condition into a con
junction of simpler subformulas\, then apply a div
erse collection of specialized decision procedures
\, first-order theorem provers\, and\, in the wors
t case\, interactive theorem provers to prove each
subformula. Techniques such as replacing complex
subformulas with stronger but simpler alterna- tiv
es\, exploiting structure inherently present in th
e verification con- ditions\, and\, when necessary
\, inserting verified lemmas and proof hints into
the imperative source code make it possible to sea
mlessly integrate all of the specialized decision
procedures and theorem provers into a single power
ful integrated reasoning system. By appropriately
applying multiple proof techniques to discharge di
fferent subformulas\, this reasoning system can ef
fectively prove the complex and challenging verifi
cation conditions that arise in this context.
LOCATION:FW11\, Computer Laboratory\, William Gates Buildin
g
CONTACT:Mike Dodds
END:VEVENT
END:VCALENDAR