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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1954)
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)
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)
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)
Bell, E.T.: Exponential numbers. American Mathematical Monthly 41, 411–419 (1934)
Bjørner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University (1998)
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)
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)
Church, A.: A note on the Entscheidungsproblem. Journal of Symbolic Logic 1, 101–102 (1936)
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)
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)
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)
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)
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. Journal of Symbolic Computation 5, 29–35 (1988)
de Bruijn, N.G.: Asymptotic Methods in Analysis. North-Holland Publishing Company, Amsterdam (1958)
Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq System Research Center (1998)
Downey, P., Sethi, R.: Assignment commands with array references. Journal of the Association for Computing Machinery 25(4), 652–666 (1978)
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)
Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2000)
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)
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)
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)
Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 332–346. Springer, Heidelberg (2002)
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)
Khachiyan, L.G.: A polynomial algorithm in linear programming. Soviet Mathematics Doklady 20, 191–194 (1979)
Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the ninth annual ACM symposium on Theory of computing, pp. 164–177 (1977)
Kreisel, G., Krivine, J.L.: Elements of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam (1967)
Krstić, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, Oregon Health and Science University (2003)
Lassez, J.-L., Mahler, M.J.: On Fourier’s algorithm for linear constraints. Journal of Automated Reasoning 9(3), 373–379 (1992)
Levitt, J.L.: Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University (1998)
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)
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)
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)
McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 62 (1962)
Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (1981)
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)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery 27(2), 356–364 (1980)
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)
Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science 12, 291–302 (1980)
Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the Association for Computing Machinery 27(3), 403–411 (1980)
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)
Papadimitriou, C.H.: On the complexity of integer programming. Journal of the Association for Computing Machinery 28(4), 765–768 (1981)
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)
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)
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)
Shankar, N., Rueß, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol. 2378, pp. 1–18. Springer, Heidelberg (2002)
Shostak, R.E.: An algorithm for reasoning about equality. Communications of the Association for Computing Machinery 21(7), 583–585 (1978)
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. Journal of the Association for Computing Machinery 26(2), 351–360 (1979)
Shostak, R.E.: Deciding combination of theories. Journal of the Association for Computing Machinery 31(1), 1–12 (1984)
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)
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)
Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. Journal of the Association for Computing Machinery 27(1), 191–205 (1980)
Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Technical Report 02-03, Department of Computer Science, University of Iowa (2002)
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)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science 290(1), 291–353 (2003)
Tiwari, A.: Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook (2000)
Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society 42, 230–265 (1936)
Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363–376. Springer, Heidelberg (2002)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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