Automatic Inference of Frame Axioms Using Static Analysis

Zvonimir Rakamaric, Alan J. Hu. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), L’Aquila, Italy.
[pdf] [bib]

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

Bibtex:

@inproceedings{ase2008-rh,
  author = {Zvonimir Rakamari\'c and Alan J. Hu},
  title = {Automatic Inference of Frame Axioms Using Static Analysis},
  booktitle = {Proceedings of the 23rd IEEE/ACM International
    Conference on Automated Software Engineering (ASE 2008)},
  publisher = {IEEE},
  year = {2008},
  pages = {89--98},
}

You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.

Comments are closed.