Inferring Invariants in Separation Logic for Imperative List-processing Programs
S. Magill, Aleksandar Nanevski, Edmund Melson Clarke, Peter Lee · 2005
An algorithm is presented for automatically inferring loop invariants in separation logic for imperative list-processing programs. A prototype implementation for a C-like lan-guage is shown to be successful in generating loop invariants for a variety of sample programs. The programs, while rela-tively 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 combination makes it possible, in principle, to solve a wider range of verification problems and makes it easier to incorpo-rate separation logic reasoning into static analysis systems, such as software model checkers. It also can provide a com-ponent of a separation-logic-based code certification system a la proof-carrying code. 1.