Unifying type checking and property checking for low-level code

We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, programspecific invariants that are difficult for traditional type checkers to express. Conversely, property checking for low-level code is challenging because it is difficult to write concise specifications that distinguish between locations in an untyped program's heap. We address both problems simultaneously by implementing a type checker for low-level code as part of our property checker. We present a low-level formalization of a C program's heap and its types that can be checked with an SMT solver, and we provide a decision procedure for checking type safety. Our type system is flexible enough to support a combination of nominal and structural subtyping for C, on a per-structure basis. We discuss several case studies that demonstrate the ability of this tool to express and check complex typ...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, Shaz Qadeer
• Keywords: Complex Type Invariants, Low-level Code, POPL 2009, Programming Languages, Type Checking