Previous shape analysis algorithms assume that the heap can be characterized in terms of reachability, that it is composed of discrete nodes that can be accessed only via access paths built from variables and field names. This assumption is violated by pointer arithmetic.
In this talk I will describe a shape analysis that works in the presence of pointer arithmetic. The abstract domain uses formulae in separation logic, leveraging that logic's non-reliance on reachability assumptions for its soundness. The analysis has been applied to verify series of programs for dynamic memory management.

This is joint work with Dino Distefano, Peter O'Hearn and Cristiano Calcagno.