Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Shape Analysis by Graph Decomposition

R. ManevichContact Information, J. BerdineContact Information, B. CookContact Information, G. RamalingamContact Information and M. SagivContact Information

(1)  Tel Aviv University,  
(2)  Microsoft Research, India
(3)  Microsoft Research Cambridge,  
Abstract
Programs commonly maintain multiple linked data structures. Correlations between multiple data structures may often be non-existent or irrelevant to verifying that the program satisfies certain safety properties or invariants. In this paper, we show how this independence between different (singly-linked) data structures can be utilized to perform shape analysis and verification more efficiently. We present a new abstraction based on decomposing graphs into sets of subgraphs, and show that, in practice, this new abstraction leads to very little loss of precision, while yielding substantial improvements to efficiency.

Contact Information R. Manevich
Email: rumster@post.tau.ac.il

Contact Information J. Berdine
Email: jjb@microsoft.com

Contact Information B. Cook
Email: bycook@microsoft.com

Contact Information G. Ramalingam
Email: grama@microsoft.com

Contact Information M. Sagiv
Email: msagiv@post.tau.ac.il
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.110 • Server: mpweb23
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)