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).
Chapter PDF
Similar content being viewed by others
References
Bagnara, R., Schachte, P.: Factorizing Equivalent Variable Pairs in ROBDDBased Implementations of Pos. In: Haeberer, A.M. (ed.) AMAST 1998. LNCS, vol. 1548, pp. 471–485. Springer, Heidelberg (1998)
Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Bryant, R.E.: On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication. IEEE Transactions on Computers 40(2), 205–213 (1991)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. Information and Compututation 98(2), 142–170 (1992)
Chandra, A.K., Markowsky, G.: On The Number of Prime Implicants. Discrete Mathematics 24(1), 7–11 (1978)
Codish, M.: Worst-Case Groundness Analysis using Positive Boolean Functions. Journal of Logic Programming 41(1), 125–128 (1999)
Coudert, O.: Two Open Questions On ROBDDs and Prime Implicants, http://www.informatik.uni-trier.de/DesignandTest/abstract30.html
Coudert, O., Madre, J.C.: Implicit and Incremental Computation of Primes and Essential Primes of Boolean Functions. In: Proceedings of the Design Automation Conference, pp. 36–39. IEEE, Los Alamitos (1992)
Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Symposium on Principles of Programming Languages, pp. 238–252 (1977)
Crama, Y., Hammer, P.L.: Boolean Functions (to appear)
Fecht, C.: Abstrakte Interpretation logischer Programme: Theorie, Implementierung, Generierung. PhD thesis, Universität des Saarlandes (1997)
Gallagher, J.P., Henriksen, K.S., Banda, G.: Techniques for Scaling Up Analyses Based on Pre-interpretations. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 280–296. Springer, Heidelberg (2005)
Heaton, A., Abo-Zaed, M., Codish, M., King, A.: A Simple Polynomial Groundness Analysis for Logic Programs. Journal of Logic Programming 45, 143–156 (2000)
Kleitman, D.J., Edelberg, M., Lubell, D.: Maximal Sized Antichains in Partial Orders. Discrete Mathematics 1(1), 47–53 (1971)
Mauborgne, L.: Abstract Interpretation Using Typed Decision Graphs. Science of Computer Programming 31(1), 91–112 (1998)
Plotkin, G.: A Note on Inductive Generalisation. Machine Intelligence 5, 153–163 (1970)
Quine, W.V.: The Problem of Simplifying Truth Functions. American Mathematical Monthly (52), 521–531 (1952)
Ravi, K., McMillan, K.L., Shiple, T.R., Somenzi, F.: Approximation and Decomposition of Binary Decision Diagrams. In: Proceedings of the Design Automation Conference, pp. 445–450. IEEE, Los Alamitos (1998)
Rudell, R.: Dynamic Variable Ordering for Ordered Binary Decision Diagrams. In: International Conference on Computer Aided Design, pp. 42–47. IEEE, Los Alamitos (1993)
Schachte, P., Søndergaard, H.: Closure Operators for ROBDDs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 1–16. Springer, Heidelberg (2005)
Shiple, T.R.: Formal Analysis of Synchronous Circuits. PhD thesis, University of California at Berkeley, Electronics Research Laboratory (1996)
Somenzi, F.: CUDD Package, Release 2.4.1., http://vlsi.colorado.edu/~fabio/
Strzemecki, T.: Polynomial-time Algorithms for Generation of Prime Implicants. ACM Journal of Complexity 8(1), 37–63 (1992)
Umans, C.: On the Complexity and Inapproximability of Shortest Implicant Problems. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 687–696. Springer, Heidelberg (1999)
Whaley, J., Lam, M.S.: Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams. In: Programming Language Design and Implementation, pp. 131–144. ACM Press, New York (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kettle, N., King, A., Strzemecki, T. (2006). Widening ROBDDs with Prime Implicants. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_7
Download citation
DOI: https://doi.org/10.1007/11691372_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)