A combination framework for tracking partition sizes

ibe an abstract interpretation based framework for proving relationships between sizes of memory partitions. Instances of this framework can prove traditional properties such as memory safety and program termination but can also establish upper bounds on usage of dynamically allocated memory. Our framework also stands out in its ability to prove properties of programs manipulating both heap and arrays which is considered a difficult task. lly, we define an abstract domain that is parameterized by an abstract domain for tracking memory partitions (sets of memory locations) and by a numerical abstract domain for tracking relationships between cardinalities of the partitions. We describe algoo construct the transfer functions for the abstract domain in terms of the corresponding transfer functions of the parameterized domains. A prototype of the framework was implemented and used to prove interesting properties of realistic programs, including programs that could not have been automatica...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Sumit Gulwani, Tal Lev-Ami, Mooly Sagiv
• Keywords: Abstract Domain, Memory Partitions, Numerical Abstract Domain, POPL 2009, Programming Languages