{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:46Z","timestamp":1749124066175},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_6","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"79-98","source":"Crossref","is-referenced-by-count":13,"title":["A Framework for Cooperating Decision Procedures"],"prefix":"10.1007","author":[{"given":"Clark W.","family":"Barrett","sequence":"first","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-63104-6_3","volume-title":"14th International Conference on Computer Aided Deduction","author":"F. Baader","year":"1997","unstructured":"Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson\u2013Oppen combination method. In: McCune, W. (ed.) 14th International Conference on Computer Aided Deduction. LNCS, pp. 19\u201333. Springer, Heidelberg (1997)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","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":"Barrett, C., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"6_CR3","unstructured":"Bjorner, N.: Integrating Decision Procedures for Temporal Verification. PhD thesis. Stanford University (1999)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer Aided Verification","author":"M.A. Colon","year":"1998","unstructured":"Colon, M.A., Uribe, T.E.: Generating finite-state abstractions of reactive systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)"},{"key":"6_CR5","unstructured":"Cyrluk, D.: Private communication (1999)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Automated Deduction - Cade-13","author":"D. Cyrluk","year":"1996","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak\u2019s Decision Procedure for Com- binations of Theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 463\u2013477. Springer, Heidelberg (1996)"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"11th International Conference on Computer-Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: 11th International Conference on Computer-Aided Verification, Trento, Italy, pp. 160\u2013172. Springer, Heidelberg (1999)"},{"key":"6_CR8","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq SRC (1998)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","first-page":"415","volume-title":"Computer Aided Verification","author":"Z. Manna","year":"1996","unstructured":"Manna, Z., et al.: STeP: Deductive-Algorithmic Verification of Reactive and Real- time Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 415\u2013418. Springer, Heidelberg (1996)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"6_CR11","unstructured":"Levitt, J.: Formal Verification Techniques for Digital Systems. PhD thesis. Stanford University (1999)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Park, D.Y.W., Skakkeb\u00e6k, J.U., Heimdahl, M.P.E., Czerny, B.J., Dill, D.L.: Checking properties of safety critical specifications using efficient decision procedures. In: FMSP 1998: Second Workshop on Formal Methods in Software Practice, March 1998, pp. 34\u201343 (1998)","DOI":"10.1145\/298595.298603"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"8","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM\u00a08, 102\u2013114 (1992)","journal-title":"Communications of the ACM"},{"key":"6_CR16","unstructured":"Ruess, H., Shankar, N.: Deconstructing Shostak. In: 17th International Conference on Computer Aided Deduction (2000)"},{"issue":"1","key":"6_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R.: Deciding combinations of theories. Journal of the Association for Computing Machinery\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Su, J., Dill, D., Skakkeb\u00e6k, J.: Formally verifying data and control with weak reachability invariants. Formal Method In Computer-Aided Design (1998)","DOI":"10.1007\/3-540-49519-3_25"},{"key":"6_CR19","series-title":"Applied Logic Series","volume-title":"1st InternationalWorkshop on Frontiers of Combining Systems (FroCoS\u201996)","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.: A new Correctness Proof of the Nelson\u2013Oppen Combination Procedure. In: Baader, F., Schulz, K. (eds.) 1st International Workshop on Frontiers of Combining Systems (FroCoS\u201996). Applied Logic Series, vol.\u00a03. Kluwer Academic Publishers, Dordrecht (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:39Z","timestamp":1556019759000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/10721959_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}