Automatic Inference of Frame Axioms Using Static Analysis

9 years 21 days ago
Automatic Inference of Frame Axioms Using Static Analysis
Many approaches to software verification are currently semi-automatic: a human must provide key logical insights — e.g., loop invariants, class invariants, and frame axioms that limit the scope of changes that must be analyzed. This paper describes a technique for automatically inferring frame axioms of procedures and loops using static analysis. The technique builds on a pointer analysis that generates limited information about all data structures in the heap. Our technique uses that information to over-approximate a potentially unbounded set of memory locations modified by each procedure/loop; this overapproximation is a candidate frame axiom. We have tested this approach on the buffer-overflow benchmarks from ASE 2007. With manually provided specifications and invariants/axioms, our tool could verify/falsify 226 of the 289 benchmarks. With our automatically inferred frame axioms, the tool could verify/falsify 203 of the 289, demonstrating the effectiveness of our approach.
Zvonimir Rakamaric, Alan J. Hu
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where KBSE
Authors Zvonimir Rakamaric, Alan J. Hu
Comments (0)