Inferring Invariants in Separation Logic for Imperative List-processing Programs

An algorithm is presented for automatically inferring loop invari- ants in separation logic for imperative list-processing programs. A prototype implementation for a C-like language is shown to be suc- cessful in generating loop invariants for a variety of sample pro- grams. The programs, while relatively small, iteratively perform destructive heap operations and hence pose problems more than challenging enough to demonstrate the utility of the approach. The invariants express information not only about the shape of the heap but also conventional properties of the program data. This com- bination makes it possible, in principle, to solve a wider range of verication problems and makes it easier to incorporate separation logic reasoning into static analysis systems, such as software model checkers. It also can provide a component of a separation-logic- based code certication system a la proof-carrying code.