Skip to main content

Widening ROBDDs with Prime Implicants: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006. Proceedings

Kettle, Neil and King, Andy and Strzemecki, Tadeusz (2006) Widening ROBDDs with Prime Implicants: 12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006. Proceedings. In: Hermanns, Holger and Palsberg, Jens, eds. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, 3920 . Springer, pp. 105-119. ISBN 978-3-540-33056-1. (doi:10.1007/11691372_7) (KAR id:37603)

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).

Item Type: Book section
DOI/Identification number: 10.1007/11691372_7
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 23:27 UTC
Last Modified: 16 Nov 2021 10:14 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/37603 (The current URI for this page, for reference purposes)

University of Kent Author Information

Kettle, Neil.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID: https://orcid.org/0000-0001-5806-4822
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.