Skip to main content
SpringerLink
Log in

Using BDDs with Combinations of Theories

  • Conference paper
  • First Online:
Book cover Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2514))

Abstract

A Boolean formula is unsatisfiable if and only if its representing binary decision diagram (BDD) is reduced to the single leaf “false”. When BDD variables represent first-order atoms including equalities between terms, uninterpreted predicates or linear arithmetic constraints, a path to the “true” leaf in the BDD might not give a model. So BDDs representing unsatisfiable quantifier-free first-order logic formulas may not reduce to the single leaf “false”. Decision procedures for combinations of theories can be used to eliminate all those unsatisfiable paths. In a naive approach every path would be considered; this would be very inefficient. We provide efficient algorithms to find general constraints (connections) from unsatisfiable paths to “true” in the BDD. Adding those connections to the BDD will eliminate many paths to “true” at one go. This procedure also ensures that no unnecessary constraint is added.

In the context of invariant validation, this gives good results when using BDDs with a rich quantifier-free language.

This work was partially funded by a grant of the “Communauté française de Belgique -Direction de la recherche scientifique - Actions de recherche concertées”.

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. W. Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954.

    Google Scholar 

  2. C. W. Barrett, D. L. Dill, and A. Stump. A generalization of Shostak’s method for combining decision procedures. In Frontiers of Combining Systems (FROCOS), volume 2309 of Lecture Notes in Computer Science. Springer-Verlag, 2002.

    Chapter  Google Scholar 

  3. N. S. Bjørner, Z. Manna, H. B. Sipma, and T. E. Uribe. Deductive verification of real-time systems using STeP. TCS: Theoretical Computer Science, 253, 2001.

    Google Scholar 

  4. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677–691, Aug. 1986.

    Google Scholar 

  5. W. Chan, R. Anderson, P. Beame, and D. Notkin. Combining constraint solving and symbolic model checking for a class of systems with non-linear constraints. In Proc. 9th Conf. Computer Aided Verification, volume 1254 of Lecture Notes in Computer Science, pages 316–327. Springer-Verlag, 1997.

    Google Scholar 

  6. K. M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, Reading, Massachusetts, 1988.

    MATH  Google Scholar 

  7. D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak’s decision procedure for combinations of theories. In Proc. 13th Int. Conf. on Automated Deduction, volume 1104 of Lecture Notes in Computer Science, pages 463–477, New Brunswick, NJ, 1996. Springer-Verlag.

    Google Scholar 

  8. J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. ICS: integrated canonizer and solver. In Proc. 13th Conf. Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 246–249. Springer-Verlag, 2001.

    Google Scholar 

  9. A. Goel, K. Sajid, H. Zhou, A. Aziz, and V. Singhal. BDD based procedures for a theory of equality with uninterpreted functions. In Proc. 10th Conf. Computer Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 244–255. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  10. J. Goubault. Proving with BDDs and control of information. In Proc. 12th Conf. on Automated Deduction, volume 814 of Lecture Notes in Computer Science, pages 499–513. Springer-Verlag, 1994.

    Google Scholar 

  11. E. P. Gribomont and D. Rossetto. CAVEAT: technique and tool for Computer Aided VErification And Transformation. In Proc. 7th Conf. on Computer Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 70–83, Liege, Belgium, 1995. Springer-Verlag.

    Google Scholar 

  12. E. P. Gribomont and N. Salloum. Using OBDD’s for the validation of Skolem verification conditions. In Proc. 16th Int. Conf. on Automated Deduction, volume 1632 of Lecture Notes in Computer Science, pages 222–226, Trento, Italy, 1999. Springer-Verlag.

    Google Scholar 

  13. J. F. Groote and J. van de Pol. Equational binary decision diagrams. In Logic Programming and Automated Reasoning, volume 1955 of Lecture Notes in Computer Science, pages 161–178. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  14. C. Heitmeyer and N. A. Lynch. The generalized railroad crossing — a case study in formal verification of real-time systems. In Proceedings 15th IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, pages 120–131, Dec. 1994.

    Google Scholar 

  15. The Liège Automata-based Symbolic Handler (LASH). Available at http://www.montefiore.ulg.ac.be/~boigelot/research/lash/.

  16. J. R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, December 1998.

    Google Scholar 

  17. N. Lynch. Distributed Algorithms. Morgan Kaufmann, San Francisco, CS, 1996.

    MATH  Google Scholar 

  18. J. Møller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In Computer Science Logic, volume 1683 of Lecture Notes in Computer Science, pages 111–125. Springer-Verlag, 1999.

    Chapter  Google Scholar 

  19. G. Nelson and D. C. Oppen. Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245–257, Oct. 1979.

    Google Scholar 

  20. G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. Journal of the ACM, 27(2):356–364, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  21. J. Posegga and P. H. Schmitt. Automated deduction with shannon graphs. Journal of Logic and Computation, 5(6):697–729, Dec. 1995.

    Google Scholar 

  22. H. Rueß and N. Shankar. Deconstructing shostak. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-01), pages 19–28, Los Alamitos, CA, 2001. IEEE Computer Society.

    Google Scholar 

  23. R. E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1–12, Jan. 1984.

    Google Scholar 

  24. C. Tinelli and M. T. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In F. Baader and K. U. Schulz, editors, Frontiers of Combining Systems: Proceedings of the 1st International Workshop (Munich, Germany), pages 103–120. Kluwer Academic Publishers, 1996.

    Google Scholar 

  25. P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of Lecture Notes in Computer Science, pages 1–19, Berlin, March 2000. Springer-Verlag.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Liège, Belgium

    Pascal Fontaine & E. Pascal Gribomont

Authors
  1. Pascal Fontaine
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. E. Pascal Gribomont
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fontaine, P., Gribomont, E.P. (2002). Using BDDs with Combinations of Theories. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00010-5

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation