'Low Level Liquid Types', Rondon, Kawaguchi and Jhala

Add to your list(s) Download to your calendar using vCal

• Andy Gordon (Microsoft Research)
• Wednesday 14 October 2009, 11:00-12:30
• FW11, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Mike Dodds.

http://pho.ucsd.edu/liquid/low_level_liquid_types_techrep_2col.pdf

We present Low-Level Liquid Types, a refinement type system for C based on Liquid Types. Low-Level Liquid Types combine refinement types with three key elements to automate verification of critical safety properties of low-level programs: First, by associating refinement types with individual heap locations and precisely tracking the locations referenced by pointers, our system is able to reason about complex invariants of in-memory data structures and sophisticated uses of pointer arithmetic. Second, by adding constructs which allow strong updates to the types of heap locations, even in the presence of aliasing, our system is able to verify properties of in-memory data structures in spite of temporary invariant violations. By using this strong update mechanism, our system is able to verify 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 safety properties without imposing an onerous annotation burden. We have implemented our approach in CSOLVE , a tool for Low-Level Liquid Type inference 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 dereferences, with a minimal annotation overhead.

This talk is part of the Program verification reading group. series.

This talk is included in these lists:

• FW11, Computer Laboratory, William Gates Building
• Program verification reading group.

Note that ex-directory lists are not shown.