Low-Level Liquid Types

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 -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 ...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala
• Keywords: Low-Level Liquid Types, POPL 2010, Programming Languages, Refinement Types, Types Combine Refinement