{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:04:10Z","timestamp":1767773050050,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":92,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_1","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"1-20","source":"Crossref","is-referenced-by-count":10,"title":["Little Engines of Proof"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Costas Courcoubetis, and David Dill. Model-checking in dense real-time. Information and Computation, 104(1):2\u201334, May 1993.","DOI":"10.1006\/inco.1993.1024"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, N. Halbwachs, T. A. Henzinger, P.-H. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1):3\u201334, 6 February 1995.","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"1_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46419-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000)","author":"K. Baukus","year":"2000","unstructured":"Kai Baukus, Saddek Bensalem, Yassine Lakhnech, and Karsten Stahl. Abstracting WS1S systems to verify parameterized networks. In Susanne Graf and Michael Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 188\u2013203, Berlin, Germany, March 2000. Springer-Verlag."},{"issue":"2","key":"1_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Clark W. Barrett, David L. Dill, and Aaron Stump. A framework for cooperating decision procedures. In David McAllester, editor, Automated Deduction\u2014CADE-17, volume 1831 of Lecture Notes in Artificial Intelligence, pages 79\u201398, Pittsburgh, PA, June 2000. Springer-Verlag.","DOI":"10.1007\/10721959_6"},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 02","author":"C. W. Barrett","year":"2002","unstructured":"Clark W. Barrett, David L. Dill, and Aaron Stump. Checking satisfiability of first-order formulas by incremental translation to SAT. In Computer-Aided Verification, CAV\u2019 02, Lecture Notes in Computer Science. Springer-Verlag, July 2002."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Leo Bachmair and Harald Ganzinger. Resolution theorem proving. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 19\u201399.","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"1_CR9","unstructured":"Nikolaj Bj\u00f8rner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999."},{"key":"1_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1\u201336, 1977.","journal-title":"Artificial Intelligence"},{"key":"1_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"S. Bensalem","year":"1998","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. Computing abstractions of infinite state systems compositionally and automatically. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 319\u2013331."},{"key":"1_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/BFb0028771","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"S. Bensalem","year":"1998","unstructured":"Saddek Bensalem, Yassine Lakhnech, and Sam Owre. InVeSt: A tool for the verification of invariants. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 505\u2013510."},{"key":"1_CR13","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, NY, 1979."},{"key":"1_CR14","volume-title":"The Correctness Problem in Computer Science","author":"R. S. Boyer","year":"1981","unstructured":"R. S. Boyer and J S. Moore. Metafunctions: Proving them correct and using them efficiently as new proof procedures. In R. S. Boyer and J S. Moore, editors, The Correctness Problem in Computer Science. Academic Press, London, 1981."},{"key":"1_CR15","unstructured":"R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study with linear arithmetic. In Machine Intelligence, volume 11. Oxford University Press, 1986."},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN\u2019 01 Conference on Programming Language Design and Implementation, 2001, pages 203\u2013313. ACM Press, 2001.","DOI":"10.1145\/378795.378846"},{"issue":"8","key":"1_CR17","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Alexander Bockmayr and Volker Weispfenning. Solving numerical constraints. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 751\u2013742.","DOI":"10.1016\/B978-044450813-3\/50014-X"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"James Corbett, Matthew Dwyer, John Hatcliff, Corina Pasareanu, Robby, Shawn Laubach, and Hongjun Zheng. Bandera: Extracting finite-state models from Java source code. In 22nd International Conference on Software Engineering, pages 439\u2013448, Limerick, Ireland, June 2000. IEEE Computer Society.","DOI":"10.1145\/337180.337234"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Shang-Ching Chou and Xiao-Shan Gao. Automated reasoning in geometry. In A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001 [RV01]}, pages 707\u2013749.","DOI":"10.1016\/B978-044450813-3\/50013-8"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Nineteenth Annual ACM Symposium on Principles of Programming Languages, pages 343\u2013354, 1992.","DOI":"10.1145\/143165.143235"},{"key":"1_CR22","unstructured":"E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999."},{"issue":"3","key":"1_CR23","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G. E. Collins","year":"1991","unstructured":"G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition. Journal of Symbolic Computation, 12(3):299\u2013328, 1991.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Second GI Conference on Automata Theory and Formal Languages","author":"G. E. Collins","year":"1975","unstructured":"G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Second GI Conference on Automata Theory and Formal Languages, number 33 in Lecture Notes in Computer Science, pages 134\u2013183, Berlin, 1975. Springer-Verlag."},{"key":"1_CR25","first-page":"91","volume":"7","author":"D. C. Cooper","year":"1972","unstructured":"D. C. Cooper. Theorem proving in arithmetic without multiplication. In Machine Intelligence 7, pages 91\u201399. Edinburgh University Press, 1972.","journal-title":"Machine Intelligence"},{"key":"1_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"M. A. Col\u00f3n","year":"1998","unstructured":"M. A. Col\u00f3n and T. E. Uribe. Generating finite-state abstractions of reactive systems using decidion procedures. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 293\u2013304."},{"key":"1_CR27","unstructured":"M. Davis. A computer program for Presburger\u2019s algorithm. In Summaries of Talks Presented at the Summer Institute for Symbolic Logic, 1957. Reprinted in Siekmann and Wrightson [SW83], pages 41\u201348."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"M. Davis. The prehistory and early history of automated deduction. In G. Wrightson, editors. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer-Verlag, 1983 [SW83]}, pages 1\u201328.","DOI":"10.1007\/978-3-642-81952-0_1"},{"key":"1_CR29","unstructured":"Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Annual IEEE Symposium on Logic in Computer Science01, pages 51\u201360. The Institute of Electrical and Electronics Engineers, 2001."},{"key":"1_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer-Aided Verification, CAV\u2019 99","author":"S. Das","year":"1999","unstructured":"Satyaki Das, David L. Dill, and Seungjoon Park. Experience with predicate abstraction. In Nicolas Halbwachs and Doron Peled, editors, Computer-Aided Verification, CAV\u2019 99, volume 1633 of Lecture Notes in Computer Science, pages 160\u2013171, Trento, Italy, July 1999. Springer-Verlag."},{"key":"1_CR31","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G. B. Dantzig","year":"1973","unstructured":"George B. Dantzig and B. Curtis Eaves. Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14:288\u2013297, 1973.","journal-title":"Journal of Combinatorial Theory (A)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394\u2013397, July 1962. Reprinted in Siekmann and Wrightson [SW83], pages 267\u2013270, 1983.","DOI":"10.1145\/368273.368557"},{"key":"1_CR33","unstructured":"David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical Report 159, COMPAQ Systems Research Center, 1998."},{"key":"1_CR34","series-title":"Lect Notes Comput Sci","volume-title":"International Conference on Automated Deduction (CADE\u201902)","author":"L. Moura de","year":"2002","unstructured":"Leonardo de Moura, Harald Rue\u00df, and Maria Sorea. Lazy theorem proving for bounded model checking over infinite domains. In A. Voronkov, editor, International Conference on Automated Deduction (CADE\u201902), Lecture Notes in Computer Science, Copenhagen, Denmark, July 2002. Springer-Verlag."},{"issue":"3","key":"1_CR35","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. JACM, 7(3):201\u2013215, 1960.","journal-title":"JACM"},{"key":"1_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/BFb0028773","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"J. Elgaard","year":"1998","unstructured":"Jacob Elgaard, Nils Klarlund, and Anders M\u00f6ller. Mona 1.x: New techniques for WS1S and WS2S. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 516\u2013520."},{"key":"1_CR37","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer-Aided Verification, CAV\u2019 2001","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"J.-C. Filli\u00e2tre, S. Owre, H. Rue\u00df, and N. Shankar. ICS: Integrated Canonization and Solving. In G. Berry, H. Comon, and A. Finkel, editors, Computer-Aided Verification, CAV\u2019 2001, volume 2102 of Lecture Notes in Computer Science, pages 246\u2013249, Paris, France, July 2001. Springer-Verlag."},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan and Shaz Qadeer. Predicate abstraction for software verification. In ACM Symposium on Principles of Programming Languages02, pages 191\u2013202. Association for Computing Machinery, January 2002.","DOI":"10.1145\/503272.503291"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Jonathan Ford and Natarajan Shankar. Formal verification of a combination decision procedure. In A. Voronkov, editor, Proceedings of CADE-19, Berlin, Germany, 2002. Springer-Verlag.","DOI":"10.1007\/3-540-45620-1_29"},{"key":"1_CR40","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1147\/rd.41.0028","volume":"4","author":"P. C. Gilmore","year":"1960","unstructured":"P. C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4:28\u201335, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 151\u2013161, 1983.","journal-title":"IBM Journal of Research and Development"},{"key":"1_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanized Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"key":"1_CR42","doi-asserted-by":"crossref","unstructured":"Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella, and Moshe Y. Vardi. Towards an efficient library for SAT: a manifesto. To appear, 2002.","DOI":"10.1016\/S1571-0653(04)00329-4"},{"key":"1_CR43","series-title":"Lect Notes Comput Sci","volume-title":"Conference on Computer Aided Verification CAV\u201997","author":"S. Graf","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi. Construction of abstract state graphs with PVS. In Conference on Computer Aided Verification CAV\u201997, LNCS 1254, Springer Verlag, 1997."},{"key":"1_CR44","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Lazy abstraction. In ACM Symposium on Principles of Programming Languages02, pages 58\u201370. Association for Computing Machinery, January 2002.","DOI":"10.1145\/565816.503279"},{"key":"1_CR45","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal Language Theory: Perspectives and Open Problems","author":"G. Huet","year":"1980","unstructured":"G. Huet and D. C. Oppen. Equations and rewrite rules: a survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349\u2013405. Academic Press, ny, 1980."},{"key":"1_CR46","series-title":"Lect Notes Comput Sci","volume-title":"Computer-Aided Verification, CAV\u2019 98","year":"1998","unstructured":"Alan J. Hu and Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag."},{"key":"1_CR47","doi-asserted-by":"crossref","unstructured":"Matt Kaufmann, Panagiotis Manolios, and J Strother Moore. Computer-Aided Reasoning: An Approach, volume 3 of Advances in Formal Methods. Kluwer, 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"1_CR48","volume-title":"Automata-Theoretic Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1993","unstructured":"R.P. Kurshan. Automata-Theoretic Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1993."},{"key":"1_CR49","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11\u201344, 1995.","journal-title":"Formal Methods in System Design"},{"key":"1_CR50","volume-title":"CSD Report STAN-CS-79-731","author":"D. C. Luckham","year":"1979","unstructured":"D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal Verifier user manual. CSD Report STAN-CS-79-731, Stanford University, Stanford, CA, March 1979."},{"key":"1_CR51","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, 1993."},{"key":"1_CR52","volume-title":"Computers and Thought","author":"M. Minsky","year":"1963","unstructured":"Marvin Minsky. Steps toward artificial intelligence. In E. A. Feigenbaum and J. Feldman, editors, Computers and Thought. McGraw-Hill Book Company, New York, 1963."},{"key":"1_CR53","doi-asserted-by":"crossref","unstructured":"Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Design Automation Conference, pages 530\u2013535, 2001.","DOI":"10.1145\/378239.379017"},{"issue":"5","key":"1_CR54","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"J. Marques-Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506\u2013521, May 1999.","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR55","series-title":"Lect Notes Comput Sci","first-page":"415","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"Z. Manna","year":"1996","unstructured":"Zohar Manna and The STeP Group. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, pages 415\u2013418, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"George C. Necula. Proof-carrying code. In 24th ACM Symposium on Principles of Programming Languages, pages 106\u2013119, Paris, France, January 1997. Association for Computing Machinery.","DOI":"10.1145\/263699.263712"},{"key":"1_CR57","volume-title":"Technical Report CSL-81-10","author":"G. Nelson","year":"1981","unstructured":"G. Nelson. Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, Ca., 1981."},{"issue":"2","key":"1_CR58","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"A. Newell, J. C. Shaw, and H. A. Simon. Empirical explorations with the logic theory machine: A case study in heuristics. In Proc. West. Joint Comp. Conf., pages 218\u2013239, 1957. Reprinted in Siekmann and Wrightson [SW83], pages 49\u201373, 1983.","DOI":"10.1007\/978-3-642-81952-0_4"},{"key":"1_CR60","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"DC Oppen","year":"1978","unstructured":"Derek C. Oppen. A $$ 2^{2^{2^{pn} } } $$ upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences, 16:323\u2013332, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752, Saratoga, NY, June 1992. Springer-Verlag.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"1_CR62","doi-asserted-by":"crossref","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","DOI":"10.1109\/32.345827"},{"key":"1_CR63","doi-asserted-by":"publisher","first-page":"163","DOI":"10.2307\/2370324","volume":"43","author":"E. L. Post","year":"1921","unstructured":"E. L. Post. Introduction to a general theory of elementary propositions. American Journal of Mathematics, 43:163\u2013185, 1921. Reprinted in [vH67, pages 264\u2013283].","journal-title":"American Journal of Mathematics"},{"key":"1_CR64","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz. An improved proof procedure. Theoria, 26:102\u2013139, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 162\u2013201, 1983.","journal-title":"Theoria"},{"key":"1_CR65","unstructured":"M. Presburger. Uber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. Compte Rendus du congr\u00e9s Math\u00e9maticiens des Pays Slaves, pages 92\u2013101, 1929."},{"issue":"8","key":"1_CR66","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102\u2013114, 1992.","journal-title":"Communications of the ACM"},{"key":"1_CR67","series-title":"Studies in Logic and the Foundations of Mathematics","first-page":"595","volume-title":"Handbook of Mathematical Logic","author":"M. O. Rabin","year":"1978","unstructured":"Michael O. Rabin. Decidable theories. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, chapter C8, pages 595\u2013629. North-Holland, Amsterdam, Holland, 1978."},{"issue":"1","key":"1_CR68","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23\u201341, 1965. Reprinted in Siekmann and Wright-son [SW83], pages 397\u2013415.","journal-title":"JACM"},{"key":"1_CR69","doi-asserted-by":"crossref","unstructured":"Harald Rue\u00df and Natarajan Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19\u201328, Boston, MA, July 2001. IEEE Computer Society.","DOI":"10.1109\/LICS.2001.932479"},{"key":"1_CR70","unstructured":"A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning. Elsevier Science, 2001."},{"key":"1_CR71","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-44755-5_3","volume-title":"Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001","author":"N. Shankar","year":"2001","unstructured":"Natarajan Shankar. Using decision procedures with a higher-order logic. In Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, volume 2152 of Lecture Notes in Computer Science, pages 5\u201326, Edinburgh, Scotland, September 2001. Springer-Verlag. Available at ftp:\/\/ftp.csl.sri.com\/pub\/users\/shankar\/tphols2001.ps.gz ."},{"key":"1_CR72","doi-asserted-by":"crossref","unstructured":"Robert E. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769\u2013779, October 1981.","DOI":"10.1145\/322276.322288"},{"key":"1_CR73","doi-asserted-by":"crossref","unstructured":"Robert E. Shostak. Deciding combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","DOI":"10.1145\/2422.322411"},{"key":"1_CR74","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/BFb0028752","volume-title":"Computer-Aided Verification, CAV\u2019 98","author":"T. R. Shiple","year":"1998","unstructured":"T. R. Shiple, J. H. Kukula, and R. K. Ranjan. A comparison of Presburger engines for EFSM reachability. In Moshe Y. Vardi, editors. Computer-Aided Verification, CAV\u2019 98, volume 1427 of Lecture Notes in Computer Science, Vancouver, Canada, June 1998. Springer-Verlag Hu and Vardi [HV98]}, pages 280\u2013292."},{"key":"1_CR75","series-title":"Lect Notes Comput Sci","first-page":"37","volume-title":"Recent Trends in Algebraic Development Techniques, WADT\u2019 99","author":"N. Shankar","year":"1999","unstructured":"Natarajan Shankar and Sam Owre. Principles and pragmatics of subtyping in PVS. In D. Bert, C. Choppy, and P. D. Mosses, editors, Recent Trends in Algebraic Development Techniques, WADT\u2019 99, volume 1827 of Lecture Notes in Computer Science, pages 37\u201352, Toulouse, France, September 1999. Springer-Verlag."},{"key":"1_CR76","series-title":"Lect Notes Comput Sci","volume-title":"International Conference on Rewriting Techniques and Applications (RTA\u2019 02)","author":"N. Shankar","year":"2002","unstructured":"N. Shankar and H. Rue\u00df. Combining Shostak theories. In International Conference on Rewriting Techniques and Applications (RTA\u2019 02), Lecture Notes in Computer Science. Springer-Verlag, July 2002. Invited Paper."},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Hassen Sa\u00efdi and Natarajan Shankar. Abstract and model check while you prove. In Computer-Aided Verification, CAV\u2019 99, Trento, Italy, July 1999.","DOI":"10.1007\/3-540-48683-6_38"},{"issue":"1","key":"1_CR78","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"Mary Sheeran and Gunnar St\u00e5lmarck","year":"2000","unstructured":"Mary Sheeran and Gunnar St\u00e5lmarck. A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods in Systems Design, 16(1):23\u201358, January 2000.","journal-title":"Formal Methods in Systems Design"},{"key":"1_CR79","series-title":"Lect Notes Comput Sci","volume-title":"6th International Conference on Automated Deduction (CADE)","author":"R. E. Shostak","year":"1982","unstructured":"R. E. Shostak, R. Schwartz, and P. M. Melliar-Smith. STP: A mechanized logic for specification and verification. In D. Loveland, editor, 6th International Conference on Automated Deduction (CADE), volume 138 of Lecture Notes in Computer Science, New York, NY, 1982. Springer-Verlag."},{"key":"1_CR80","doi-asserted-by":"crossref","unstructured":"J. Siekmann and G. Wrightson, editors. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81952-0"},{"key":"1_CR81","unstructured":"A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1948."},{"key":"1_CR82","doi-asserted-by":"crossref","unstructured":"Cesare Tinelli and Mehdi Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Frans Baader and Klaus U. Schulz, editors, Frontiers of Combining Systems: First International Workshop, volume 3 of Applied Logic Series, pages 103\u2013119, Munich, Germany, March 1996. Kluwer.","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"1_CR83","doi-asserted-by":"crossref","unstructured":"Laurent Th\u00e9ry. A certified version of Buchberger\u2019s algorithm. In H. Kirchner and C. Kirchner, editors, Proceedings of CADE-15, number 1421 in Lecture Notes in Artificial Intelligence, pages 349\u2013364, Berlin, Germany, July 1998. Springer-Verlag.","DOI":"10.1007\/BFb0054271"},{"key":"1_CR84","unstructured":"Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000."},{"key":"1_CR85","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002","author":"A. Tiwari","year":"2002","unstructured":"Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In C.J. Tomlin and M.R. Greenstreet, editors, Hybrid Systems: Computation and Control, 5th International Workshop, HSCC 2002, volume 2289 of Lecture Notes in Computer Science, pages 465\u2013478, Stanford, CA, March 2002. Springer-Verlag."},{"volume-title":"From Frege to G\u00f6del: A Sourcebook of Mathematical Logic, 1879-1931","year":"1967","key":"1_CR86","unstructured":"J. van Heijenoort, editor. From Frege to G\u00f6del: A Sourcebook of Mathematical Logic, 1879-1931. Harvard University Press, Cambridge, MA, 1967."},{"key":"1_CR87","unstructured":"Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings 1st Annual IEEE Symp. on Logic in Computer Science, pages 332\u2013344. IEEE Computer Society Press, 1986."},{"issue":"4","key":"1_CR88","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1145\/367177.367224","volume":"3","author":"H. Wang","year":"1960","unstructured":"H. Wang. Proving theorems by pattern recognition \u2014 I. Communications of the ACM, 3(4):220\u2013234, 1960. Reprinted in Siekmann and Wrightson [SW83], pages 229\u2013243, 1983.","journal-title":"Communications of the ACM"},{"key":"1_CR89","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H. Wang","year":"1960","unstructured":"Hao Wang. Toward mechanical mathematics. IBM Journal, 4:2\u201322, 1960.","journal-title":"IBM Journal"},{"key":"1_CR90","doi-asserted-by":"crossref","unstructured":"H. Wang. Mechanical mathematics and inferential analysis. In P. Braffort and D. Hershberg, editors, Computer Programming and Formal Systems. North-Holland, 1963.","DOI":"10.1016\/S0049-237X(08)72016-0"},{"key":"1_CR91","doi-asserted-by":"crossref","unstructured":"Richard W. Weyhrauch. Prolegomena to a theory of mechanized formal reasoning. Artificial Intelligence, 13(1 and 2):133\u2013170, April 1980.","DOI":"10.1016\/0004-3702(80)90015-6"},{"key":"1_CR92","doi-asserted-by":"crossref","unstructured":"Hantao Zhang. SATO: An efficient propositional prover. In Conference on Automated Deduction, pages 272\u2013275, 1997.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T11:09:36Z","timestamp":1737025776000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":92,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}