Partitioned memory models for program analysis

Wei Wang, Clark Barrett, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
EditorsAhmed Bouajjani, David Monniaux
PublisherSpringer Verlag
Number of pages20
ISBN (Print)9783319522333
StatePublished - 2017
Event18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, France
Duration: Jan 15 2017Jan 17 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10145 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Partitioned memory models for program analysis'. Together they form a unique fingerprint.

Cite this