Smallfoot: Static Assertion Checking for C programs

Pointers have long been one of the dark corners of programming languages. Tractable proof and analysis tools are lacking for all but the most simple, shallow, properties of the program heap. A recent theory, separation logic, has shed fresh light on this area, and has generated considerable interest worldwide. It has lead to much simpler by-hand specifications and program proofs than previous formalisms, and it suggests, for the first time, the possibility of scalable analysis methods for expressive heap properties. To date, though, separation logic remains mainly a theoretical advance; there are no tools based on separation logic for any real programming languages.We propose to develop a static assertion checker for C based on separation logic. Separation logic works naturally with a low-level RAM model, and thus appears to be well suited to code that must run close to the hardware without an intermediate abstraction of the kind found in the runtimes of high-level languages such as ML or Java. Much fundamental code of this sort is written in the C programming language, and is outside the effective range of current tools.Our tool, Smallfoot, will accept precondition and postcondition assertions written in separation logic, and programs will be checked using a combination of symbolic execution and specialized proof procedures. Abstract interpretation will be used to alleviate the need to state invariants. We will check structural integrity properties of programs -- such as that data structures are in consistent states, or that resource boundaries are respected -- rather than full functional correctness. In this way we hope to keep specifications simple, and to achieve a high degree of automation. As it is aimed at low-level programs, Smallfoot will be complementary to static assertion checkers for higher-level languages such as the ESC tool for Java and the Spec# tool for C#.Success on the problems in this project could have a significant impact on the use of logic to check properties of systems programs.