Partitioned memory models for program analysis

Wei Wang, Clark Barrett, Thomas Wies

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

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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
EditorsAhmed Bouajjani, David Monniaux
PublisherSpringer Verlag
Pages539-558
Number of pages20
ISBN (Print)9783319522333
DOIs
StatePublished - Jan 1 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

Other

Other18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
CountryFrance
CityParis
Period1/15/171/17/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Wang, W., Barrett, C., & Wies, T. (2017). Partitioned memory models for program analysis. In A. Bouajjani, & D. Monniaux (Eds.), Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings (pp. 539-558). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-52234-0_29