@inproceedings{0d90c10275a2424fac8f36d49e52f46b,
title = "Partitioned memory models for program analysis",
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{\textquoteright}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.",
author = "Wei Wang and Clark Barrett and Thomas Wies",
year = "2017",
doi = "10.1007/978-3-319-52234-0_29",
language = "English (US)",
isbn = "9783319522333",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "539--558",
editor = "Ahmed Bouajjani and David Monniaux",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings",
note = "18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 ; Conference date: 15-01-2017 Through 17-01-2017",
}