Arithmetic Strengthening for Shape Analysis

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...

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook
• Keywords: Arithmetic Analysis, Arithmetic Program, Formal Methods, SAS 2007, Shape Analysis