{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:29:21Z","timestamp":1778297361745,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540662020","type":"print"},{"value":"9783540486831","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48683-6_39","type":"book-chapter","created":{"date-parts":[[2007,10,7]],"date-time":"2007-10-07T03:22:18Z","timestamp":1191727338000},"page":"455-469","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Deciding Equality Formulas by Small Domains Instantiations"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoav","family":"Rodeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Shtrichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Siegel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,1,14]]},"reference":[{"key":"39_CR1","unstructured":"W. Ackerman. Solvable cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954."},{"key":"39_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Proc. CAV\u201994","author":"J. R. Burch","year":"1994","unstructured":"J. R. Burch and D. L. Dill. Automatic verification of pipelined microprocessor control. In Proc. CAV\u201994, LNCS 818, pp 68\u201380."},{"key":"39_CR3","doi-asserted-by":"crossref","unstructured":"R. Bryant, S. German, and M. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In this volume, 1999.","DOI":"10.1007\/3-540-48683-6_40"},{"key":"39_CR4","unstructured":"The Sacres Consortium. Safety critical embedded systems: from requirements to system architecture, 1995. Esprit Project Description EP 20.897, URL \nhttp:\/\/www.tni.fr\/sacres\n\n."},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"R. Hojati, A. Isles, D. Kirkpatrick, and R.K. Brayton. Verification using uninterpreted functions and finite instantiations. FMCAD\u201996, pp 218\u2013232.","DOI":"10.1007\/BFb0031810"},{"key":"39_CR6","unstructured":"R. Hojati, A. Kuehlmann, S. German, and R. Brayton. Validity checking in the theory of equality using finite instantiations. In Proc. Intl. Workshop on Logic Synthesis, 1997."},{"key":"39_CR7","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. An efficient algorithm for the range minimization problem. Tech. report, Weizmann Institute, 1998."},{"key":"39_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/BFb0055057","volume-title":"ICALP98","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli, M. Siegel, and O. Shtrichman. Translation validation for synchronous languages. ICALP98 LNCS 1443, pages 235\u2013246"},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)-automatic verification of a compilation process. Intl. journal on Software Tools for Technology Transfer (STTT), vol 2, 1999.","DOI":"10.1007\/s100090050027"},{"key":"39_CR10","series-title":"Lect Notes Comput Sci","first-page":"244","volume-title":"CAV\u201998","author":"[. K. Sajid","year":"1998","unstructured":"[SGZ+98]_ K. Sajid, A. Goel, H. Zhou, A. Aziz, S. Barber, and V. Singhal. BDD based procedures for a theory of equality with uninterpreted functions. CAV\u201998, LNCS 1427, pp 244\u2013255."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48683-6_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T06:03:23Z","timestamp":1586153003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48683-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662020","9783540486831"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-48683-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"14 January 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}