{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T16:02:44Z","timestamp":1780675364025,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642007675","type":"print"},{"value":"9783642007682","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00768-2_16","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:16:10Z","timestamp":1238116570000},"page":"174-177","source":"Crossref","is-referenced-by-count":189,"title":["Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays"],"prefix":"10.1007","author":[{"given":"Robert","family":"Brummayer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Babic, D.: Exploiting Structure for Scalable Software Verification. PhD thesis (2008)"},{"key":"16_CR2","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: SMT-Comp. (2008), http:\/\/www.smtcomp.org"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Biere, A.: PicoSAT essentials. JSAT\u00a04 (2008)","DOI":"10.3233\/SAT190039"},{"key":"16_CR4","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. In: Proc.\u00a0SMT (2008)","DOI":"10.1145\/1512464.1512467"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: Bit-precise modelling of word-level problems for model checking. In: Proc.\u00a0BPR (2008)","DOI":"10.1145\/1512464.1512472"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-69850-0_1","volume-title":"25 Years of Model Checking","author":"E.M. Clarke","year":"2008","unstructured":"Clarke, E.M.: The birth of model checking. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol.\u00a05000, pp. 1\u201326. Springer, Heidelberg (2008)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR9","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Proc.\u00a0SAT (2002)"},{"key":"16_CR10","volume-title":"Decision Procedures: An algorithmic Point of View","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An algorithmic Point of View. Springer, Heidelberg (2008)"},{"key":"16_CR11","unstructured":"Ranise, S., Tinelli, C.: The satisfiability modulo theories library, SMT-LIB (2008), http:\/\/www.smt-lib.org"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Sebastiani, R.: Lazy satisfiability modulo theories. JSAT, 3 (2007)","DOI":"10.3233\/SAT190034"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00768-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T03:49:05Z","timestamp":1589687345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00768-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642007675","9783642007682"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}