
Open access
Date
2014Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
Eective static analyses of heap-manipulating programs need to track precise information about the heap structures and the values computed by the program. Most existing heap analyses rely on man- ual annotations to precisely analyze general and, in particular, recursive, heap structures. Moreover, they either do not exploit value information to obtain more precise heap information or require more annotations for this purpose. In this paper, we present a combined heap and value anal- ysis that infers complex invariants for recursive heap structures such as lists and trees, including relations between value elds of heap-allocated objects. Our analysis uses a novel notion of edge-local identiers to track value information about the source and target of a pointer, even if these are summary nodes. With each potential pointer in the heap, our analysis associates value information that describes in which states the pointer may exist, and uses this information to improve the precision of the analysis by pruning infeasible heap structures. Our analysis has been implemented in the static analyzer Sample; experimental results show that it can automatically infer invariants for data structures, for which state-of-the-art analyses require manual annotations. Show more
Permanent link
https://doi.org/10.3929/ethz-a-010235205Publication status
publishedJournal / series
Technical report / Department of Computer SciencePublisher
ETH-ZürichEdition / version
[Updated version from 15. September 2014]Subject
CODING (SOFTWARE ENGINEERING); PROCESS MANAGEMENT (OPERATING SYSTEMS); SPECIAL PROGRAMMING METHODS; PROZESSVERWALTUNG + PROZESSMANAGEMENT (BETRIEBSSYSTEME); SPEZIELLE PROGRAMMIERMETHODEN; KODIERUNG (SOFTWARE ENGINEERING)Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science
Notes
See also: http://e-citations.ethbib.ethz.ch/view/pub:115133.More
Show all metadata
ETH Bibliography
yes
Altmetrics