Partitioned Memory Models for Program Analysis

Partitioned Memory Models for Program Analysis” by Wei Wang, Clark Barrett, and Thomas Wies. In Proceedings of the 22^nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '16), 2016. Submitted for review.

Abstract

Scalability is a key challenge in static analysis. For imperative languages like C, the approach taken for modeling memory can play a significant role in scalability. In this paper, we explore a family of memory models called partitioned memory models which divide memory up based on the results of a points-to analysis. We review Steensgaard's original and field-sensitive points-to analyses and introduce a new cell-based field-sensitive analysis which extends the benefits of field-sensitive analysis to program data allocated on the heap. We give experimental results on benchmarks from the software verification competition using the Cascade program verification framework. We show that the cellbased field-sensitive memory model significantly improves the performance of Cascade, making it competitive with other state-of-the-art C analysis tools.

BibTeX entry:

@inproceedings{WBW16,
   author = {Wei Wang and Clark Barrett and Thomas Wies},
   title = {Partitioned Memory Models for Program Analysis},
   booktitle = {Proceedings of the {\it 22^{nd}} International Conference
	on Tools and Algorithms for the Construction and Analysis of
	Systems (TACAS '16)},
   year = {2016},
   note = {Submitted for review},
   url = {http://www.cs.nyu.edu/~barrett/pubs/WBW16.pdf}
}

(This webpage was created with bibtex2web.)