School of Computing

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},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014