Points-to analysis using BDDs

This paper reports on a new approach to solving a subset-based points-to analysis for Java using Binary Decision Diagrams (BDDs). In the model checking community, BDDs have been shown very effective for representing large sets and solving very large verification problems. Our work shows that BDDs can also be very effective for developing a points-to analysis that is simple to implement and that scales well, in both space and time, to large programs. The paper first introduces BDDs and operations on BDDs using some simple points-to examples. Then, a complete subset-based points-to algorithm is presented, expressed completely using BDDs and BDD operations. This algorithm is then refined by finding appropriate variable orderings and by making the algorithm propagate sets incrementally, in order to arrive at a very efficient algorithm. Experimental results are given to justify the choice of variable ordering, to demonstrate the improvement due to incrementalization, and to compare th...

• Type: Conference
• Year: 2003
• Where: PLDI
• Authors: Marc Berndl, Ondrej Lhoták, Feng Qian, Laurie J. Hendren, Navindra Umanee
• Keywords: Binary Decision Diagrams, PLDI 2003, Points-to Analysis, Programming Languages, Subset-based Points-to