Numeric inference of heap shapes for the automated analysis of heap-allocating programs

More about the book

This thesis presents a novel approach to the analysis of heap-allocating programs that is based solely on abstract numeric domains. In contrast to approaches that require the user to provide so-called instrumentation predicates, our analysis is geared towards the automatic inference of heap invariants. Using off-the-shelf relational numeric domains, we infer invariants that relate the shape of heap-allocated data structures to their numeric content. Our analysis is implemented as a stack of functor domains and is shown to be able to infer invariants that distinguish between lists, trees and arbitrary graphs, thereby allowing for the automatic verification of standard algorithms.