Shape analysis for composite data structures

Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, Hongseok Yang

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

Abstract

We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include "cyclic doubly-linked lists of acyclic singly-linked lists", "singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes", etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 19th International Conference, CAV 2007, Proceedings
Pages178-192
Number of pages15
Volume4590 LNCS
StatePublished - 2007
Event19th International Conference on Computer Aided Verification, CAV 2007 - Berlin, Germany
Duration: Jul 3 2007Jul 7 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4590 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other19th International Conference on Computer Aided Verification, CAV 2007
CountryGermany
CityBerlin
Period7/3/077/7/07

Fingerprint

Shape Analysis
Composite Structures
Predicate
Data structures
Data Structures
Safety
Driver
Composite materials
Higher Order
Safety Analysis
Head
Equipment and Supplies
Manipulation
Data storage equipment
Unknown
Evaluate
Vertex of a graph
Experiment
Experiments

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Berdine, J., Calcagno, C., Cook, B., Distefano, D., O'Hearn, P. W., Wies, T., & Yang, H. (2007). Shape analysis for composite data structures. In Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings (Vol. 4590 LNCS, pp. 178-192). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4590 LNCS).

Shape analysis for composite data structures. / Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O'Hearn, Peter W.; Wies, Thomas; Yang, Hongseok.

Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Vol. 4590 LNCS 2007. p. 178-192 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4590 LNCS).

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

Berdine, J, Calcagno, C, Cook, B, Distefano, D, O'Hearn, PW, Wies, T & Yang, H 2007, Shape analysis for composite data structures. in Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. vol. 4590 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4590 LNCS, pp. 178-192, 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, 7/3/07.
Berdine J, Calcagno C, Cook B, Distefano D, O'Hearn PW, Wies T et al. Shape analysis for composite data structures. In Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Vol. 4590 LNCS. 2007. p. 178-192. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Berdine, Josh ; Calcagno, Cristiano ; Cook, Byron ; Distefano, Dino ; O'Hearn, Peter W. ; Wies, Thomas ; Yang, Hongseok. / Shape analysis for composite data structures. Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings. Vol. 4590 LNCS 2007. pp. 178-192 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c989dd3db7c44a499e5bbc106bf5ed8c,
title = "Shape analysis for composite data structures",
abstract = "We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include {"}cyclic doubly-linked lists of acyclic singly-linked lists{"}, {"}singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes{"}, etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.",
author = "Josh Berdine and Cristiano Calcagno and Byron Cook and Dino Distefano and O'Hearn, {Peter W.} and Thomas Wies and Hongseok Yang",
year = "2007",
language = "English (US)",
isbn = "3540733671",
volume = "4590 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "178--192",
booktitle = "Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings",

}

TY - GEN

T1 - Shape analysis for composite data structures

AU - Berdine, Josh

AU - Calcagno, Cristiano

AU - Cook, Byron

AU - Distefano, Dino

AU - O'Hearn, Peter W.

AU - Wies, Thomas

AU - Yang, Hongseok

PY - 2007

Y1 - 2007

N2 - We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include "cyclic doubly-linked lists of acyclic singly-linked lists", "singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes", etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.

AB - We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include "cyclic doubly-linked lists of acyclic singly-linked lists", "singly-linked lists of cyclic doubly-linked lists with back-pointers to head nodes", etc. The analysis introduces the use of generic higher-order inductive predicates describing spatial relationships together with a method of synthesizing new parameterized spatial predicates which can be used in combination with the higher-order predicates. In order to evaluate the proposed approach for realistic programs we have performed experiments on examples drawn from device drivers: the analysis proved safety of the data structure manipulation of several routines belonging to an IEEE 1394 (firewire) driver, and also found several previously unknown memory safety bugs.

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

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

M3 - Conference contribution

AN - SCOPUS:38149070828

SN - 3540733671

SN - 9783540733676

VL - 4590 LNCS

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

SP - 178

EP - 192

BT - Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings

ER -