@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",
doi = "10.1007/978-3-540-73368-3_22",
language = "English (US)",
isbn = "3540733671",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "178--192",
booktitle = "Computer Aided Verification - 19th International Conference, CAV 2007, Proceedings",
note = "19th International Conference on Computer Aided Verification, CAV 2007 ; Conference date: 03-07-2007 Through 07-07-2007",
}