Skip to main content
SpringerLink
Log in

Combining Decision Procedures

  • Chapter
Formal Methods at the Crossroads. From Panacea to Foundational Support

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2757))

Abstract

We give a detailed survey of the current state-of-the-art methods for combining decision procedures. We review the Nelson-Oppen combination method, Shostak method, and some very recent results on the combination of theories over non-disjoint signatures.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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.

Similar content being viewed by others

References

  1. Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1954)

    MATH  Google Scholar 

  2. Baader, F., Schulz, K.U.: Combining constraint solving. In: Comon, H., Marché, C., Treinen, R. (eds.) CCL 1999. LNCS, vol. 2002, pp. 104–158. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Barrett, C.W., Dill, D.L., Levitt, J.L.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 187–201. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  4. Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak’s method for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 132–146. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Bell, E.T.: Exponential numbers. American Mathematical Monthly 41, 411–419 (1934)

    Article  MathSciNet  Google Scholar 

  6. Bjørner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University (1998)

    Google Scholar 

  7. Bjørner, N.S., Browne, A., Colón, M., Finkbeiner, B., Manna, Z., Sipma, H.B., Uribe, T.E.: Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design 16(3), 227–270 (2000)

    Article  Google Scholar 

  8. Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 127–137. Springer, Heidelberg (2000)

    Google Scholar 

  9. Church, A.: A note on the Entscheidungsproblem. Journal of Symbolic Logic 1, 101–102 (1936)

    Article  MATH  Google Scholar 

  10. Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

    Google Scholar 

  11. Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 7, pp. 91–99. Edinburgh University Press (1972)

    Google Scholar 

  12. Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B., Saaltink, M.: EVES: An overview. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol. 552, pp. 389–405. Springer, Heidelberg (1991)

    Google Scholar 

  13. Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak’s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 463–477. Springer, Heidelberg (1996)

    Google Scholar 

  14. Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5, 29–35 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  15. de Bruijn, N.G.: Asymptotic Methods in Analysis. North-Holland Publishing Company, Amsterdam (1958)

    MATH  Google Scholar 

  16. Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq System Research Center (1998)

    Google Scholar 

  17. Downey, P., Sethi, R.: Assignment commands with array references. Journal of the Association for Computing Machinery 25(4), 652–666 (1978)

    MATH  MathSciNet  Google Scholar 

  18. Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. Journal of the Association for Computing Machinery 27(4), 758–771 (1980)

    MATH  MathSciNet  Google Scholar 

  19. Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2000)

    Google Scholar 

  20. Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM Journal on Computing 4(1), 69–76 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  21. Filliâtre, J.-C., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 246–249. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: Karp, R.M. (ed.) Complexity of Computation. SIAM-AMS proceedings, vol. 7, pp. 27–42. American Mathematical Society (1974)

    Google Scholar 

  23. Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–346. Springer, Heidelberg (2002)

    Google Scholar 

  24. Kapur, D.: A rewrite rule based framework for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol. 2309, pp. 87–102. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  25. Khachiyan, L.G.: A polynomial algorithm in linear programming. Soviet Mathematics Doklady 20, 191–194 (1979)

    MATH  Google Scholar 

  26. Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the ninth annual ACM symposium on Theory of computing, pp. 164–177 (1977)

    Google Scholar 

  27. Kreisel, G., Krivine, J.L.: Elements of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam (1967)

    MATH  Google Scholar 

  28. Krstić, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, Oregon Health and Science University (2003)

    Google Scholar 

  29. Lassez, J.-L., Mahler, M.J.: On Fourier’s algorithm for linear constraints. Journal of Automated Reasoning 9(3), 373–379 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  30. Levitt, J.L.: Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University (1998)

    Google Scholar 

  31. Levy, B., Filippenko, I., Marcus, L., Menas, T.: Using the state delta verification system (SDVS) for hardware verification. In: Melham, T.F., Stavridou, V., Boute, R.T. (eds.) Theorem Prover in Circuit Design: Theory, Practice and Experience, pp. 337–360. Elsevier Science, Amsterdam (1992)

    Google Scholar 

  32. Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford pascal verifier user manual. Technical Report STAN-CS-79-731, Stanford University (1979)

    Google Scholar 

  33. Matiyasevich, Y.V.: Diophantine representation of recursively enumerable predicates. In: Fenstad, J.E. (ed.) Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 171–177. North-Holland Publishing Company, Amsterdam (1971)

    Chapter  Google Scholar 

  34. McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 62 (1962)

    Google Scholar 

  35. Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (1981)

    Google Scholar 

  36. Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics, vol. 29, pp. 201–211. American Mathematical Society (1984)

    Google Scholar 

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

    Article  MATH  Google Scholar 

  38. Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)

    MATH  MathSciNet  Google Scholar 

  39. Oppen, D.C.: A \(2^{2^{2^{pn}}}\)upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences 16(3), 323–332 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  40. Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)

    Article  MATH  MathSciNet  Google Scholar 

  41. Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the Association for Computing Machinery 27(3), 403–411 (1980)

    MATH  MathSciNet  Google Scholar 

  42. Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996)

    Google Scholar 

  43. Papadimitriou, C.H.: On the complexity of integer programming. Journal of the Association for Computing Machinery 28(4), 765–768 (1981)

    MATH  MathSciNet  Google Scholar 

  44. Presburger, M.: Über die vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. In: Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, pp. 92–101 (1929)

    Google Scholar 

  45. Ringeissen, C.: Cooperation of decision procedures for the satisfiability problem. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. Applied Logic Series, vol. 3, pp. 121–140. Kluwer Academic Publishers, Dordrecht (1996)

    Google Scholar 

  46. Rueß, H., Shankar, N.: Deconstructing Shostak. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 19–28. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  47. Shankar, N., Rueß, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–18. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  48. Shostak, R.E.: An algorithm for reasoning about equality. Communications of the Association for Computing Machinery 21(7), 583–585 (1978)

    MATH  MathSciNet  Google Scholar 

  49. Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. Journal of the Association for Computing Machinery 26(2), 351–360 (1979)

    MATH  MathSciNet  Google Scholar 

  50. Shostak, R.E.: Deciding combination of theories. Journal of the Association for Computing Machinery 31(1), 1–12 (1984)

    MATH  MathSciNet  Google Scholar 

  51. Stump, A., Barret, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 500–504. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  52. Stump, A., Barret, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  53. Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. Journal of the Association for Computing Machinery 27(1), 191–205 (1980)

    MATH  MathSciNet  Google Scholar 

  54. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)

    Google Scholar 

  55. Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Technical Report 02-03, Department of Computer Science, University of Iowa (2002)

    Google Scholar 

  56. Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. Applied Logic Series, vol. 3, pp. 103–120. Kluwer Academic Publishers, Dordrecht (1996)

    Google Scholar 

  57. Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290(1), 291–353 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  58. Tiwari, A.: Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook (2000)

    Google Scholar 

  59. Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 42, 230–265 (1936)

    Article  MATH  Google Scholar 

  60. Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363–376. Springer, Heidelberg (2002)

    Google Scholar 

  61. Zarba, C.G.: A tableau calculus for combining non-disjoint theories. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 315–329. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Stanford University,  

    Zohar Manna & Calogero G. Zarba

Authors
  1. Zohar Manna
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Calogero G. Zarba
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Software Technology, Graz University of Technology, Austria

    Bernhard K. Aichernig

  2. Department of Computing and Software, McMaster University, 1280 Main St West, L8S 4K1, Hamilton, ON, Canada

    Tom Maibaum

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Manna, Z., Zarba, C.G. (2003). Combining Decision Procedures. In: Aichernig, B.K., Maibaum, T. (eds) Formal Methods at the Crossroads. From Panacea to Foundational Support. Lecture Notes in Computer Science, vol 2757. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40007-3_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-40007-3_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20527-2

  • Online ISBN: 978-3-540-40007-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation