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

Full description

Saved in:
Bibliographic Details
Main Authors: Rakamaric, Z., Hu, A.J.
Format: Conference Proceeding
Language:English
Subjects:
Arrays
Data structures
Resource management
Scalability
Shape
Software
Specification languages
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 over- approximation 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.
ISSN:1938-4300
2643-1572
DOI:10.1109/ASE.2008.19