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

(NYU-CS-TR910)

Authors: Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, and
Clark Barrett

Abstract:
It is well known that the use of points-to information can 
substantially improve the accuracyof 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.