{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:05:02Z","timestamp":1777125902327,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642047718","type":"print"},{"value":"9783642047725","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-04772-5_40","type":"book-chapter","created":{"date-parts":[[2009,9,23]],"date-time":"2009-09-23T20:32:44Z","timestamp":1253737964000},"page":"304-311","source":"Crossref","is-referenced-by-count":13,"title":["Effective Bit-Width and Under-Approximation"],"prefix":"10.1007","author":[{"given":"Robert","family":"Brummayer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"40_CR1","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: SMT-Comp (2008), www.smtcomp.org"},{"key":"40_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2002","unstructured":"Barrett, C., Dill, D., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"key":"40_CR3","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (June 2008), www.SMT-LIB.org"},{"key":"40_CR4","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"A. Bradley","year":"2007","unstructured":"Bradley, A., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"40_CR5","volume-title":"Proc.\u00a0SMT 2008","author":"R. Brummayer","year":"2008","unstructured":"Brummayer, R., Biere, A.: Lemmas on Demand for the Extensional Theory of Arrays. In: Proc.\u00a0SMT 2008, ACM Press, New York (2008)"},{"key":"40_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"TACAS 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505. Springer, Heidelberg (2009)"},{"key":"40_CR7","volume-title":"Proc.\u00a0BPR 2008","author":"R. Brummayer","year":"2008","unstructured":"Brummayer, R., Biere, A., Lonsing, F.: BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking. In: Proc.\u00a0BPR 2008. ACM Press, New York (2008)"},{"key":"40_CR8","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S., Strichman, O., Brady, B.: Deciding Bit-Vector Arithmetic with Abstraction. Software Tools for Technology Transfer, STTT (2009)"},{"key":"40_CR9","unstructured":"Claessen, K., S\u00f6rensson, N.: New Techniques that Improve MACE-style Finite Model Finding. In: CADE-19, Workshop W4, Model Computation \u2013 Principles, Algorithms, Applications (2003)"},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-Guided Abstraction Refinement for Symbolic Model Checking. Journal of the ACM, JACM (2003)","DOI":"10.1145\/876638.876643"},{"key":"40_CR11","volume-title":"Proc.\u00a0SAT 2002","author":"L. Moura de","year":"2002","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on Demand for Satisfiability Solvers. In: Proc.\u00a0SAT 2002. Springer, Heidelberg (2002)"},{"key":"40_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Saxe, J.: Theorem Proving Using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"40_CR13","unstructured":"Ganesh, V.: Decision Procedures for Bit-Vectors, Arrays and Integers. PhD thesis, Computer Science Department, Stanford University (2007)"},{"key":"40_CR14","volume-title":"Proc.\u00a0ICCD","author":"N. He","year":"2007","unstructured":"He, N., Hsiao, M.: Bounded Model Checking of Embedded Software in Wireless Cognitive Radio Systems. In: Proc.\u00a0ICCD. IEEE, Los Alamitos (2007)"},{"key":"40_CR15","volume-title":"Proc.\u00a0BPR 2008","author":"N. He","year":"2008","unstructured":"He, N., Hsiao, M.: A new Testability Guided Abstraction to Solving Bit-Vector Formula. In: Proc.\u00a0BPR 2008. ACM, New York (2008)"},{"key":"40_CR16","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":"40_CR17","doi-asserted-by":"crossref","unstructured":"Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation (JSAT)\u00a03 (2007)","DOI":"10.3233\/SAT190034"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory - EUROCAST 2009"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04772-5_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,22]],"date-time":"2020-05-22T12:11:45Z","timestamp":1590149505000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04772-5_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642047718","9783642047725"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04772-5_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}