Efficient ROBDD Operations for Program Analysis

Peter Schachte
Department of Computer Science, The University of Melbourne, Parkville 3052, Australia.


Reduced Ordered Binary Decision Diagrams (ROBDDs), also known as Bryant graphs, are a representation for Boolean functions supporting many efficient operations. Because of this, they have often been used to implement the positive Boolean functions for program analysis. Some ROBDD operations heavily used in program analysis, however, are still rather expensive. The undertaking of the present paper is to develop some more efficient algorithms for a few key ROBDD operations used in program analysis.
Conference Home Page