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

Program Analysis
Memory Model
Data storage equipment
Data Structures
Scalability
Data structures
Software Verification
Program Verification
Heap
Cell
Static Analysis
Casting
Model Analysis
Cascade
Divides
Static analysis
Benchmark
Experimental Results
Modeling

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

Partitioned memory models for program analysis. / Wang, Wei; Barrett, Clark; Wies, Thomas.

Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Vol. 10145 LNCS Springer Verlag, 2017. p. 539-558 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS).

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

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, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10145 LNCS, Springer Verlag, pp. 539-558, 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, Paris, France, 1/15/17. https://doi.org/10.1007/978-3-319-52234-0_29
Wang W, Barrett C, Wies T. Partitioned memory models for program analysis. In Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Vol. 10145 LNCS. Springer Verlag. 2017. p. 539-558. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-52234-0_29
Wang, Wei ; Barrett, Clark ; Wies, Thomas. / Partitioned memory models for program analysis. Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings. Vol. 10145 LNCS Springer Verlag, 2017. pp. 539-558 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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’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",
volume = "10145 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "539--558",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Partitioned memory models for program analysis

AU - Wang, Wei

AU - Barrett, Clark

AU - Wies, Thomas

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85010693183&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85010693183&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-52234-0_29

DO - 10.1007/978-3-319-52234-0_29

M3 - Conference contribution

SN - 9783319522333

VL - 10145 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 539

EP - 558

BT - Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings

PB - Springer Verlag

ER -