{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:57:07Z","timestamp":1725490627317},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540733676"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_33","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T18:29:34Z","timestamp":1188412174000},"page":"294-297","source":"Crossref","is-referenced-by-count":1,"title":["C32SAT: Checking C Expressions"],"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":[{"unstructured":"Biere, A.: The evolution from LIMMAT to NANOSAT. Technical Report 444, Dept. Computer Science, ETH Z\u00fcrich (2004)","key":"33_CR1"},{"unstructured":"Biere, A.: Occurrence lists for 2-watched literal schemes (submitted)","key":"33_CR2"},{"doi-asserted-by":"crossref","unstructured":"Biere, A., Sinz, C.: Decomposing sat problems into connected components. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 2 (2006)","key":"33_CR3","DOI":"10.3233\/SAT190022"},{"unstructured":"Brummayer, R., Biere, A.: Local two-level And-Inverter Graph minimization without blowup. In: MEMICS 2006. Proceedings of the 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (2006)","key":"33_CR4"},{"unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Proceedings of TACAS 2007, Springer, Heidelberg (to appear, 2007)","key":"33_CR5"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-Cprograms. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 570\u2013574. Springer, Heidelberg (2005)"},{"key":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/11513988_30","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2005","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Cogent: Accurate theorem proving for program verification. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 296\u2013300. Springer, Heidelberg (2005)"},{"unstructured":"ISO\/IEC. Programming languages - C (ISO\/IEC 9899:1999(E)) (1999)","key":"33_CR9"},{"issue":"12","key":"33_CR10","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust boolean reasoning for equivalence checking and functional property verification. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11817963_17","volume-title":"Computer Aided Verification","author":"N. Sethi","year":"2006","unstructured":"Sethi, N., Barret, C.: Cascade: C assertion checker and deductive engine. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 166\u2013169. Springer, Heidelberg (2006)"},{"doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in the propositional calculus. Studies in constructive mathematics and mathematical logic, pp. 115\u2013125 (1968)","key":"33_CR12","DOI":"10.1007\/978-1-4899-5327-8_25"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:14:03Z","timestamp":1605744843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_33","relation":{},"subject":[]}}