Partitioned Memory Models for Program Analysis

“Partitioned Memory Models for Program Analysis” by Wei Wang, Clark Barrett, and Thomas Wies. In Proceedings of the 18^th International Conference on Verification, Model Checking, and Abstract Interpretion (VMCAI '17), (Ahmed Bouajjani and David Monniaux, eds.), Jan. 2017, pp. 539-558. Paris, France.

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 as well as Data Structure Analysis (DSA), and introduce a new cell-based points-to analysis which more precisely handles heap data structures and type-unsafe operations like pointer arithmetic and pointer casting. We give experimental results on benchmarks from the software verification competition using the program verification framework in Cascade. We show that a partitioned memory model using our cell-based points-to analysis outperforms models using other analyses.

BibTeX entry:

@inproceedings{WBW17,
   author = {Wei Wang and Clark Barrett and Thomas Wies},
   editor = {Ahmed Bouajjani and David Monniaux},
   title = {Partitioned Memory Models for Program Analysis},
   booktitle = {Proceedings of the {\it 18^{th}} International Conference
	on Verification, Model Checking, and Abstract Interpretion (VMCAI
	'17)},
   pages = {539--558},
   publisher = {Springer International Publishing},
   month = jan,
   year = {2017},
   isbn = {978-3-319-52234-0},
   doi = {10.1007/978-3-319-52234-0_29},
   note = {Paris, France},
   url = {http://theory.stanford.edu/~barrett/pubs/WBW17.pdf}
}

(This webpage was created with bibtex2web.)