Automatic Numeric Abstractions for Heap-Manipulating Programs

Stephen Magill

A number of safety and liveness questions of programs involving heap-based data structures can be phrased as questions about numeric properties of those structures. A data structure traversal might terminate if the length of some path is eventually zero; a function to remove n elements from a collection may only be safe if the collection has size at least n. I will discuss an automatic method for producing numeric abstractions of heap-manipulating programs that is sound for both termination and safety reasoning. The numeric abstractions are expressed as simple imperative programs over integer variables and have the property that termination and safety of the numeric program ensures termination and safety of the original, heap-manipulating program. The translation makes use of a shape analysis based on separation logic and has support for user-deļ¬ned inductive data structures.