{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:01:05Z","timestamp":1742392865981},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_22","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T14:39:50Z","timestamp":1265899190000},"page":"246-249","source":"Crossref","is-referenced-by-count":65,"title":["ICS: Integrated Canonizer and Solver?"],"prefix":"10.1007","author":[{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sam","family":"Owre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Harald","family":"Rue*B","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natarajan","family":"Shankar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"22_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 (FMCAD\u2019 96)","author":"C. Barrett","year":"1996","unstructured":"Clark Barrett, David Dill, and Jeremy Levitt. Validity checking for combinations of theories with equality. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD\u2019 96), volume 1166 of Lecture Notes in Computer Science, pages 187\u2013201, Palo Alto, CA, November 1996. Springer-Verlag."},{"issue":"4","key":"22_CR2","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Matt Kaufmann and J Strother Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203\u2013213, April 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-49519-3_4","volume-title":"Formal Methods in Computer-Aided Design (FM-CAD\u2019 98)","author":"O. M\u00f6ller","year":"1998","unstructured":"O. M\u00f6ller and H. Rue*B. Solving bit-vector equations. In G. Gopalakrishnan and Ph. Windley, editors, Formal Methods in Computer-Aided Design (FM-CAD\u2019 98), volume 1522 of Lecture Notes in Computer Science, pages 36\u201348, Palo Alto, CA, November 1998. Springer-Verlag."},{"key":"22_CR4","series-title":"Lect Notes Comput Sci","first-page":"415","volume-title":"Computer Aided Verification (CAV 96)","author":"Z. Manna","year":"1996","unstructured":"Z. Manna and the STeP group. STeP: Deductive-algorithmic verification of reactive and real-time systems. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification (CAV 96), volume 1102 of Lecture Notes in Computer Science, pages 415\u2013418, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"22_CR5","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":"22_CR6","unstructured":"Harald Rue*B and N. Shankar. Deconstructing Shostak. To be presented at LICS\u20192001, available from \n                    http:\/\/www.csl.sri.com\/papers\/lics01\/\n                    \n                  , 2001."},{"issue":"1","key":"22_CR7","doi-asserted-by":"publisher","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 ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,23]],"date-time":"2019-02-23T15:02:02Z","timestamp":1550934122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}