Skip to main content
SpringerLink
Log in

Closure Operators for ROBDDs

  • Conference paper
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3855))

Abstract

Program analysis commonly makes use of Boolean functions to express information about run-time states. Many important classes of Boolean functions used this way, such as the monotone functions and the Boolean Horn functions, have simple semantic characterisations. They also have well-known syntactic characterisations in terms of Boolean formulae, say, in conjunctive normal form. Here we are concerned with characterisations using binary decision diagrams. Over the last decade, ROBDDs have become popular as representations of Boolean functions, mainly for their algorithmic properties. Assuming ROBDDs as representation, we address the following problems: Given a function ψ and a class of functions Δ, how to find the strongest ϕεΔ entailed by ψ (when such a ϕ is known to exist)? How to find the weakest ϕεΔ that entails ψ? How to determine that a function ψ belongs to a class Δ? Answers are important, not only for several program analyses, but for other areas of computer science, where Boolean approximation is used. We give, for many commonly used classes Δ of Boolean functions, algorithms to approximate functions represented as ROBDDs, in the sense described above. The algorithms implement upper closure operators, familiar from abstract interpretation. They immediately lead to algorithms for deciding class membership.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Armstrong, T., Marriott, K., Schachte, P., Søndergaard, H.: Two classes of Boolean functions for dependency analysis. Science of Computer Programming 31(1), 3–45 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  2. Brace, K., Rudell, R., Bryant, R.: Efficient implementation of a BDD package. In: Proc. Twenty-seventh ACM/IEEE Design Automation Conf., pp. 40–45 (1990)

    Google Scholar 

  3. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers C–35(8), 677–691 (1986)

    Article  Google Scholar 

  4. Bryant, R.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys 24(3), 293–318 (1992)

    Article  Google Scholar 

  5. Codish, M., Søndergaard, H., Stuckey, P.J.: Sharing and groundness dependencies in logic programs. ACM Transactions on Programming Languages and Systems 21(5), 948–976 (1999)

    Article  Google Scholar 

  6. Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Description of Programming Concepts, pp. 237–277. North-Holland, Amsterdam (1978)

    Google Scholar 

  7. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Sixth ACM Symp. Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)

    Chapter  Google Scholar 

  8. Ekin, O., Foldes, S., Hammer, P.L., Hellerstein, L.: Equational characterizations of Boolean function classes. Discrete Mathematics 211, 27–51 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  9. Genaim, S., King, A.: Goal-independent suspension analysis for logic programs with dynamic scheduling. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 84–98. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  10. Giacobazzi, R.: Semantic Aspects of Logic Program Analysis. PhD thesis, University of Pisa, Italy (1993)

    Google Scholar 

  11. Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Programming Languages and Systems 20(5), 1067–1109 (1998)

    Article  Google Scholar 

  12. Glynn, K., Stuckey, P.J., Sulzmann, M., Søndergaard, H.: Exception analysis for non-strict languages. In: Proc. 2002 ACM SIGPLAN Int. Conf. Functional Programming, pp. 98–109. ACM Press, New York (2002)

    Chapter  Google Scholar 

  13. Halmos, P.R.: Lectures on Boolean Algebras. Springer, Heidelberg (1963)

    MATH  Google Scholar 

  14. Heaton, A., Abo-Zaed, M., Codish, M., King, A.: A simple polynomial groundness analysis for logic programs. J. Logic Programming 45(1-3), 143–156 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  15. Howe, J.M., King, A.: Efficient groundness analysis in Prolog. Theory and Practice of Logic Programming 3(1), 95–124 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  16. Howe, J.M., King, A., Lu, L.: Analysing logic programs by reasoning backwards. In: Bruynooghe, M., Lau, K.-K. (eds.) Program Development in Computational Logic. LNCS, vol. 3049, pp. 152–188. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  17. Marriott, K., Søndergaard, H.: Precise and efficient groundness analysis for logic programs. ACM Lett. Programming Languages and Systems 2(1–4), 181–196 (1993)

    Article  Google Scholar 

  18. Mycroft, A.: Abstract Interpretation and Optimising Transformations for Applicative Programs. PhD thesis, University of Edinburgh, Scotland (1981)

    Google Scholar 

  19. Ore, O.: Combinations of closure relations. Ann. Math. 44(3), 514–533 (1943)

    Article  MathSciNet  Google Scholar 

  20. Post, E.L.: The Two-Valued Iterative Systems of Mathematical Logic. Princeton University Press, Princeton (1941); Reprinted in Davis, M.: Solvability, Provability, Definability: The Collected Works of Emil L. Post, pp. 249–374. Birkhaüser (1994)

    Google Scholar 

  21. Rudeanu, S.: Boolean Functions and Equations. North-Holland, Amsterdam (1974)

    MATH  Google Scholar 

  22. Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. Tenth Ann. ACM Symp. Theory of Computing, pp. 216–226 (1978)

    Google Scholar 

  23. Ward, M.: The closure operators of a lattice. Ann. Math. 43(2), 191–196 (1942)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Software Engineering, The University of Melbourne, Vic. 3010, Australia

    Peter Schachte & Harald Søndergaard

Authors
  1. Peter Schachte
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Harald Søndergaard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Aiken Computation Laboratory, Harvard University,, 02138, Cambridge, Mass, USA

    E. Allen Emerson

  2. Bell Laboratories, Alcatel-Lucent,  

    Kedar S. Namjoshi

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schachte, P., Søndergaard, H. (2005). Closure Operators for ROBDDs. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_1

Download citation

  • DOI: https://doi.org/10.1007/11609773_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-31139-3

  • Online ISBN: 978-3-540-31622-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation