{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T08:38:12Z","timestamp":1789979892998,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540433811","type":"print"},{"value":"9783540459880","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45988-x_11","type":"book-chapter","created":{"date-parts":[[2007,6,6]],"date-time":"2007-06-06T22:19:02Z","timestamp":1181168342000},"page":"132-146","source":"Crossref","is-referenced-by-count":25,"title":["A Generalization of Shostak#x2019;s Method for Combining Decision Procedures"],"prefix":"10.1007","author":[{"given":"Clark W.","family":"Barrett","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity Checking for Combinations of Theories with Equality. In M. Srivas and A. Camilleri, eds., Formal Methods in Computer-Aided Design, volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201. Springer-Verlag, 1996."},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","volume-title":"A Framework for Cooperating Decision Procedures","author":"C. Barrett","year":"2000","unstructured":"C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In 17th International Conference on Automated Deduction, Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"11_CR3","unstructured":"Clark W. Barrett. Checking Validity of Quantifier-Free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University, 2002."},{"key":"11_CR4","unstructured":"Nikolaj S. Bj\u00f8rner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University, 1999."},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"13th International Conference on Computer Aided Deduction","author":"D. Cyrluk","year":"1996","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak\u2019s Decision Procedure for Combinations of Theories. In M. McRobbie and J. Slaney, eds., 13th International Conference on Computer Aided Deduction, volume 1104 of Lecture Notes in Computer Science, pages 463\u2013477. Springer-Verlag, 1996."},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","first-page":"415","volume-title":"STeP: Deductive-Algorithmic Verification of Reactive and Realtime Systems","author":"Z. Manna","year":"1996","unstructured":"Z. Manna et al. STeP: Deductive-Algorithmic Verification of Reactive and Realtime Systems. In 8th International Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 415\u2013418. Springer-Verlag, 1996."},{"key":"11_CR7","unstructured":"Jeremy R. Levitt. Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University, 1999."},{"issue":"2","key":"11_CR8","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u201357, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D. C. Oppen","year":"1980","unstructured":"Derek C. Oppen. Complexity, Convexity and Combinations of Theories. Theoretical Computer Science, 12:291\u2013302, 1980.","journal-title":"Theoretical Computer Science"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, ed., 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748\u2013752. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"H. Ruess and N. Shankar. Deconstructing Shostak. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 19\u201328, June 2001.","DOI":"10.1109\/LICS.2001.932479"},{"issue":"1","key":"11_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"Robert E. Shostak. Deciding Combinations of Theories. Journal of the Association for Computing Machinery, 31(1):1\u201312, 1984.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"C. Tinelli and M. Harandi. A New Correctness Proof of the Nelson-Oppen Combination Procedure. In F. Baader and K. Schulz, eds., 1st International Workshop on Frontiers of Combining Systems (FroCoS\u201996), volume 3 of Applied Logic Series. Kluwer Academic Publishers, 1996.","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"11_CR14","unstructured":"Ashish Tiwari. Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook, 2000."}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45988-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T01:01:55Z","timestamp":1550365315000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45988-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433811","9783540459880"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-45988-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}