A Note on the Soundness of Difference Propagation
Difference propagation is an algorithm widely used in points-to and alias analysis. To the best of our knowledge, the soundness of the version of the algorithm used for the static analysis of Java programs has not yet been proven. An attempt to do this yields a surprise: when the algorithm is used to compute field sensitive points-to for Java programs, soundness cannot be guaranteed when self-loads (statements of the kind x=x.f) are present. We discuss such a scenario and suggest a modification of the algorithm that is sufficient to prove soundness.
Tue 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:25
|A Mechanical Soundness Proof for Subtyping Over Recursive Types|
FTfJPDOI Pre-print File Attached
|A formal account of SSA in Java-like languages|
|A Note on the Soundness of Difference Propagation|