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

Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors

Christopher L. ConwayContact Information, Dennis DamsContact Information, Kedar S. NamjoshiContact Information and Clark BarrettContact Information

(1)  Dept. of Computer Science, New York University,  
(2)  Bell Laboratories, Alcatel-Lucent,  
Abstract
It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound only for memory-safe programs. Thus, it appears problematic to utilize points-to information to verify the memory safety property without giving up soundness. We show that a sound combination is possible, even if the points-to information is computed separately and only conditionally sound. This result is based on a refined statement of the soundness conditions of points-to analyses and a general mechanism for composing conditionally sound analyses.

Contact Information Christopher L. Conway
Email: cconway@cs.nyu.edu

Contact Information Dennis Dams
Email: dennis@research.bell-labs.com

Contact Information Kedar S. Namjoshi
Email: kedar@research.bell-labs.com

Contact Information Clark Barrett
Email: barrett@cs.nyu.edu
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.114 • Server: mpweb07
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)