Arithmetic Strengthening for Shape Analysis

Stephen Magill, Josh Berdine, Edmund M. Clarke, and Byron Cook

Abstract

Shape analyses are often imprecise in their numerical reasoning, whereas numerical static analyses are often largely unaware of the shape of a program's heap. In this paper we propose a lazy method of combining a shape analysis based on separation logic with an arbitrary arithmetic analysis. When potentially spurious counterexamples are reported by our shape analysis, the method constructs a purely arithmetic program whose traces over-approximate the set of counterexample traces. It then uses this arithmetic program together with the arithmetic analysis to construct a refinement for the shape analysis. Our method is aimed at proving properties that require comprehensive reasoning about heaps together with more targeted arithmetic reasoning. Given a sufficient precondition, our technique can automatically prove memory safety of programs whose error-free operation depends on a combination of shape, size, and integer invariants. We have implemented our algorithm and tested it on a number of common list routines using a variety of arithmetic analysis tools for refinement.

Details

Publication typeInproceedings
Published inStatic Analysis, 14th International Symposium, SAS 2007, Kongens Lyngby, Denmark, August 22-24, 2007, Proceedings
Pages419-436
Volume4634
SeriesLecture Notes in Computer Science
ISBN978-3-540-74060-5
PublisherSpringer Verlag
> Publications > Arithmetic Strengthening for Shape Analysis