{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:12Z","timestamp":1761611172790},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031808","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"187-201","source":"Crossref","is-referenced-by-count":82,"title":["Validity checking for combinations of theories with equality"],"prefix":"10.1007","author":[{"given":"Clark","family":"Barrett","sequence":"first","affiliation":[]},{"given":"David","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Jeremy","family":"Levitt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"J. R. Burch and D. L. Dill, \u201cAutomatic Verification of Microprocessor Control\u201d, In Computer Aided Verification, 6th International Conference, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, P. Lincoln and N. Shankar, \u201cOn Shostak's Decision Procedure for Combinations of Theories\u201d, Proceedings of the 13th International Conference on Automated Deduction, New Brunswick, NJ, July 1996, 463\u2013477.","DOI":"10.1007\/3-540-61511-3_107"},{"issue":"1","key":"13_CR3","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1093\/comjnl\/34.1.2","volume":"34","author":"A. J. J. Dick","year":"1991","unstructured":"A. J. J. Dick, \u201cAn Introduction to Knuth-Bendix Completion\u201d, The Computer Journal 34(1):2\u201315, 1991.","journal-title":"The Computer Journal"},{"issue":"4","key":"13_CR4","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P. J. Downey","year":"1980","unstructured":"P. J. Downey, R. Sethi and R. E. Tarjan, \u201cVariations on the Common Subexpression Problem\u201d, Journal of the ACM, 27(4):758\u2013771, 1980.","journal-title":"Journal of the ACM"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar, \u201cExperiments in Theorem Proving and Model Checking for Protocol Verification\u201d, In Proceedings of Formal Methods Europe, March 1996, 662\u2013681.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"R. B. Jones, D. L. Dill and J. R. Burch, \u201cEfficient Validity Checking for Processor Verification\u201d, IEEE\/ACM International Conference on Computer Aided Design, 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. B. Bendix, \u201cSimple Word Problems in Universal Algebras\u201d, In Computational Problems in Abstract Algebra, ed. J. Leech, 263\u2013297, Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"13_CR8","volume-title":"Technique Report STAN-CS-TR-94","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, et al., \u201cSTeP: the Stanford Temporal Prover\u201d, Technique Report STAN-CS-TR-94, Computer Science Department, Stanford, 1994."},{"issue":"2","key":"13_CR9","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen, \u201cSimplification by Cooperating Decision Procedures\u201d, ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"13_CR10","unstructured":"G. Nelson, D. Detlefs, K. R. M. Leino and J. Saxe, \u201cExtended Static Checking Home page\u201d, \u2329URL:http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html\u232a, 1996."},{"issue":"2","key":"13_CR11","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, et al., \u201cFormal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS\u201d, IEEE Transactions of Software Engineering, 21(2):107\u2013125, 1995.","journal-title":"IEEE Transactions of Software Engineering"},{"issue":"7","key":"13_CR12","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. E. Shostak","year":"1978","unstructured":"R. E. Shostak, \u201cAn Algorithm for Reasoning About Equality\u201d, Communications of the ACM, 21(7):583\u2013585, 1978.","journal-title":"Communications of the ACM"},{"issue":"1","key":"13_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. E. Shostak","year":"1984","unstructured":"R. E. Shostak, \u201cDeciding Combinations of Theories\u201d, Journal of the ACM, 31(1):1\u201312, 1984.","journal-title":"Journal of the ACM"},{"issue":"2","key":"13_CR14","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R. E. Tarjan","year":"1975","unstructured":"R. E. Tarjan, \u201cEfficiency of a Good but not Linear Set Union Algorithm\u201d, Journal of the ACM, 22(2):215\u2013225, 1975.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031808","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:49:39Z","timestamp":1586612979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031808"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0031808","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}