© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Widening ROBDDs with Prime Implicants
Neil Kettle, Andy King, and Tadeusz Strzemecki
In Holger Hermanns and Jens Palsberg, editors, Twelfth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 3920 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, March 2006 Also see http://www.springer.de/comp/lncs/index.html.Abstract
Despite the ubiquity of ROBDDs in program analysis, and extensive literature on ROBDD minimisation, there is a dearth of work on approximating ROBDDs. The need for approximation arises because many ROBDD operations result in an ROBDD whose size is quadratic in the size of the inputs. Furthermore, if ROBDDs are used in abstract interpretation, the running time of the analysis is related not only to the complexity of the individual ROBDD operations but also the number of operations applied. The number of operations is, in turn, constrained by the number of times a Boolean function can be weakened before stability is achieved. This paper proposes a widening that can be used to both constrain the size of an ROBDD and also ensure that the number of times that it is weakened is bounded by some given constant. The widening can be used to either systematically approximate from above (i.e. derive a weaker function) or below (i.e. infer a stronger function).
Download publication 460 kbytes (PostScript)Bibtex Record
@inproceedings{2327, author = {Neil Kettle and Andy King and Tadeusz Strzemecki}, title = {Widening {ROBDD}s with {P}rime {I}mplicants}, month = {March}, year = {2006}, pages = {182-196}, keywords = {determinacy analysis, Craig interpolants}, note = {Also see http://www.springer.de/comp/lncs/index.html}, doi = {}, url = {http://www.cs.kent.ac.uk/pubs/2006/2327}, publication_type = {inproceedings}, submission_id = {23106_1134995465}, booktitle = {Twelfth International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, editor = {Holger Hermanns and Jens Palsberg}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, refereed = {yes}, volume = {3920}, }