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
PublisherSpringer Verlag
Pages539-558
Number of pages20
Volume10145 LNCS
ISBN (Print)9783319522333
DOIs
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)03029743
ISSN (Electronic)16113349

Other

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

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Wang, W., Barrett, C., & Wies, T. (2017). Partitioned memory models for program analysis. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings (Vol. 10145 LNCS, 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