Shape analysis for composite data structures
Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn P, Wies T, Yang H. 2007. Shape analysis for composite data structures. 19th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 4590, 178–192.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Berdine, Josh;
Calcagno, Cristiano;
Cook, Byron;
Distefano, Dino;
O'Hearn, Peter;
Wies, ThomasISTA;
Yang, Hongseok
Series Title
LNCS
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.
Publishing Year
Date Published
2007-01-01
Proceedings Title
19th International Conference on Computer Aided Verification
Publisher
Springer
Volume
4590
Page
178 - 192
Conference
CAV: Computer Aided Verification
Conference Location
Berlin, Germany
Conference Date
2007-07-03 – 2007-07-07
IST-REx-ID
Cite this
Berdine J, Calcagno C, Cook B, et al. Shape analysis for composite data structures. In: 19th International Conference on Computer Aided Verification. Vol 4590. Springer; 2007:178-192. doi:10.1007/978-3-540-73368-3_22
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P., Wies, T., & Yang, H. (2007). Shape analysis for composite data structures. In 19th International Conference on Computer Aided Verification (Vol. 4590, pp. 178–192). Berlin, Germany: Springer. https://doi.org/10.1007/978-3-540-73368-3_22
Berdine, Josh, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O’Hearn, Thomas Wies, and Hongseok Yang. “Shape Analysis for Composite Data Structures.” In 19th International Conference on Computer Aided Verification, 4590:178–92. Springer, 2007. https://doi.org/10.1007/978-3-540-73368-3_22.
J. Berdine et al., “Shape analysis for composite data structures,” in 19th International Conference on Computer Aided Verification, Berlin, Germany, 2007, vol. 4590, pp. 178–192.
Berdine J, Calcagno C, Cook B, Distefano D, O’Hearn P, Wies T, Yang H. 2007. Shape analysis for composite data structures. 19th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 4590, 178–192.
Berdine, Josh, et al. “Shape Analysis for Composite Data Structures.” 19th International Conference on Computer Aided Verification, vol. 4590, Springer, 2007, pp. 178–92, doi:10.1007/978-3-540-73368-3_22.
Google Scholar