{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:17:34Z","timestamp":1759033054786},"reference-count":4,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,10,26]],"date-time":"2013-10-26T00:00:00Z","timestamp":1382745600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1007\/s10817-013-9295-4","type":"journal-article","created":{"date-parts":[[2013,10,25]],"date-time":"2013-10-25T17:29:36Z","timestamp":1382722176000},"page":"453-456","source":"Crossref","is-referenced-by-count":8,"title":["\u201cDecision Procedures: An Algorithmic Point of View,\u201d by Daniel Kroening and Ofer Strichman, Springer-Verlag, 2008"],"prefix":"10.1007","volume":"51","author":[{"given":"Clark","family":"Barrett","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,10,26]]},"reference":[{"key":"9295_CR1","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer Berlin Heidelberg (2007)"},{"key":"9295_CR2","unstructured":"Kroening, D., Strichman, O.: http:\/\/www.decision-procedures.org\/ . Accessed Oct 2013"},{"key":"9295_CR3","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design 2009, pp. 45\u201352. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"7","key":"9295_CR4","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9295-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9295-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9295-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:52Z","timestamp":1559265712000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9295-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,26]]},"references-count":4,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["9295"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9295-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,10,26]]}}}