Efficient ROBDD Operations for Program Analysis
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