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

“Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors” by Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and Clark Barrett. In Proceedings of the 15^th International Static Analysis Symposium (SAS '08), (Mara Alpuente and Germán Vidal, eds.), July 2008, pp. 62-77. Valencia, Spain.

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.

BibTeX entry:

@inproceedings{CDN+08,
   author = {Christopher L. Conway and Dennis Dams and Kedar S. Namjoshi
	and Clark Barrett},
   editor = {Mara Alpuente and Germ{\'a}n Vidal},
   title = {Pointer Analysis, Conditional Soundness, and Proving the
	Absence of Errors},
   booktitle = {Proceedings of the {\it 15^{th}} International Static
	Analysis Symposium (SAS '08)},
   series = {Lecture Notes in Computer Science},
   volume = {5079},
   pages = {62--77},
   publisher = {Springer},
   month = jul,
   year = {2008},
   note = {Valencia, Spain},
   url = {http://theory.stanford.edu/~barrett/pubs/CDN+08.pdf}
}

(This webpage was created with bibtex2web.)