Automatic numeric abstractions for heap-manipulating programs
Journal
Conference Record of the Annual ACM Symposium on Principles of Programming Languages
Pages
211-222
Date Issued
2010
Author(s)
Abstract
We present a logic for relating heap-manipulating programs to numeric abstractions. These numeric abstractions are expressed as simple imperative programs over integer variables and have the property that termination and safety of the numeric program ensures termination and safety of the original, heap-manipulating program. We have implemented an automated version of this abstraction process and present experimental results for programs involving a variety of data structures.
SDGs
Type
conference paper