BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:'Low Level Liquid Types'\, Rondon\, Kawaguchi and Jhala - Andy Gor
 don (Microsoft Research)
DTSTART:20091014T100000Z
DTEND:20091014T113000Z
UID:TALK19892@talks.cam.ac.uk
CONTACT:Mike Dodds
DESCRIPTION:http://pho.ucsd.edu/liquid/low_level_liquid_types_techrep_2col
 .pdf\n\nWe present Low-Level Liquid Types\, a refinement type system for C
  based on Liquid Types. Low-Level Liquid Types combine refinement types wi
 th three key elements to automate verification of critical safety properti
 es of low-level programs: First\, by associating refinement types with ind
 ividual heap locations and precisely tracking the locations referenced by 
 pointers\, our system is able to reason about complex invariants of in-mem
 ory data structures and sophisticated uses of pointer arithmetic. Second\,
  by adding constructs which allow strong updates to the types of heap loca
 tions\, even in the presence of aliasing\, our system is able to verify pr
 operties of in-memory data structures in spite of temporary invariant viol
 ations. By using this strong update mechanism\, our system is able to veri
 fy the correct initialization of newly-allocated regions of memory. Third\
 , by using the abstract interpretation framework of Liquid Types\, we are 
 able to use refinement type inference to automatically verify important sa
 fety properties without imposing an onerous annotation burden. We have imp
 lemented our approach in CSOLVE\, a tool for Low-Level Liquid Type inferen
 ce for C programs. We demonstrate through several examples that CSOLVE is 
 able to precisely infer complex invariants required to verify impor- tant 
 safety properties\, like the absence of array bounds violations and NULL d
 ereferences\, with a minimal annotation overhead.
LOCATION:FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR