Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Bringing LTL Model Checking to Biologists Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Partitioned Memory Models for Program Analysis

verfasst von : Wei Wang, Clark Barrett, Thomas Wies

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel IC3 - Flipping the E in ICE
Fußnoten
1
A formal presentation of the semantics of the partitioned memory model is presented in [28].
 
2
We borrow this term from Miné [19], but use it in a different context. Miné aimed to build a cell-based abstract domain for value analysis, while we target a cell-based points-to analysis.
 
3
They can be handled using a straightforward adaptation of Steensgaard’s approach.
 
4
Cascade placed 3rd in the Heap Data Structures category of SV-COMP 2016 [4].
 
5
We used a context-insensitive version of DSA to make a fair comparison because the other analyses are also context-insensitive. Context sensitivity could be added to any of them, improving the results.
 
Literatur
1.
Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis, University of Copenhagen, May 1994
2.
Balatsouras, G., Smaragdakis, Y.: Structure-sensitive points-to analysis for C and C++. In: Static Analysis Symposium (SAS) (2016)
3.
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard - version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (SMT) (2010)
4.
Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (reported on SV-COMP 2016). In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2016)
5.
Böhme, S., Moskal, M.: Heaps, data structures: a challenge for automated provers. In: Conference on Automated Deduction (CADE) (2011)
6.
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Mach. Intell. 7, 23–50 (1972)MATH
7.
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2004)
8.
Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. Electron. Notes Theor. Comput. Sci. (ENTCS) 254, 85–103 (2009)CrossRef
9.
Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (POPL) (2009)
10.
Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C.: Pointer analysis, conditional soundness, and proving the absence of errors. In: Static Analysis Symposium (SAS) (2008)
11.
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C a software analysis perspective. In: Software Engineering and Formal Methods (SEFM) (2012)
12.
Foster, J.S., Fähndrich, M., Aiken, A.: Flow-insensitive points-to analysis with term and set constraints. Technical report CSD-97-964, University of California, Berkeley (1997)
13.
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Computer Aided Verification (CAV) (2015)
14.
Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Program Analysis for Software Tools and Engineering (PASTE) (2001)
15.
Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL) (2008)
16.
Lahiri, S.K., Qadeer, S., Rakamarić, Z.: Static and precise detection of concurrency errors in systems code using SMT solvers. In: Computer Aided Verification (CAV) (2009)
17.
Lal, A., Qadeer, S.: Powering the static driver verifier using Corral. In: Foundations of Software Engineering (FSE) (2014)
18.
Lattner, C., Lenharth, A., Adve, V.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Programming Language Design and Implementation (PLDI) (2007)
19.
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Language, Compilers, and Tool Support for Embedded Systems (LCTES) (2006)
20.
Morse, J., Ramalho, M., Cordeiro, L., Nicole, D., Fischer, B.: ESBMC 1.22 (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2014)
21.
Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: Principles of Programming Languages (POPL) (2002)
22.
Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis for C. In: Program Analysis for Software Tools and Engineering (PASTE) (2004)
23.
Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis of C. ACM Trans. Program. Lang. Syst. 30(1), 4 (2007)CrossRef
24.
Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Computer Aided Verification (CAV) (2015)
25.
Rakamarić, Z., Hu, A.J.: A scalable memory model for low-level code. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2009)
26.
Steensgaard, B.: Points-to analysis by type inference of programs with structures and unions. In: Compiler Construction (CC) (1996)
27.
Steensgaard, B.: Points-to analysis in almost linear time. In: Principles of Programming Languages (POPL) (1996)
28.
Wang, W.: Partition memory models for program analysis. Ph.D. thesis, New York University, May 2016
29.
Wang, W., Barrett, C., Wies, T.: Cascade 2.0. In: Verification, Model Checking, and Abstract Interpretation (VMCAI) (2014)
30.
Yong, S.H., Horwitz, S., Reps, T.: Pointer analysis for programs with structures and casting. In: Programming Language Design and Implementation (PLDI) (1999)
Metadaten
Titel
Partitioned Memory Models for Program Analysis
verfasst von
Wei Wang
Clark Barrett
Thomas Wies
Copyright-Jahr
2017
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-52234-0_29