{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:36Z","timestamp":1777890996198,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642277047","type":"print"},{"value":"9783642277054","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_12","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T17:18:06Z","timestamp":1327511886000},"page":"146-161","source":"Crossref","is-referenced-by-count":82,"title":["LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IR"],"prefix":"10.1007","author":[{"given":"Florian","family":"Merz","sequence":"first","affiliation":[]},{"given":"Stephan","family":"Falke","sequence":"additional","affiliation":[]},{"given":"Carsten","family":"Sinz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"12_CR1","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A. Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. STTT\u00a011(1), 69\u201383 (2009)","journal-title":"STTT"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Babi\u0107, D., Hu, A.J.: Calysto: Scalable and precise extended static checking. In: Proc. ICSE 2008, pp. 211\u2013220 (2008)","DOI":"10.1145\/1368088.1368118"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Brummayer, R.D.: Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. Ph.D. thesis, Johannes Kepler Universit\u00e4t, Linz, Austria (2009)","DOI":"10.1007\/978-3-642-00768-2_16"},{"issue":"2","key":"12_CR6","first-page":"142","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. IC\u00a098(2), 142\u2013170 (1992)","journal-title":"IC"},{"key":"12_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI 2008, pp. 209\u2013224 (2008)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"12_CR9","first-page":"85","volume":"254","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. ENTCS\u00a0254, 85\u2013103 (2009)","journal-title":"ENTCS"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: Proc. ASE 2009, pp. 137\u2013148 (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-642-23702-7_26","volume-title":"Static Analysis","author":"A.F. Donaldson","year":"2011","unstructured":"Donaldson, A.F., Haller, L., Kroening, D., R\u00fcmmer, P.: Software Verification using k-Induction. In: Yahav, E. (ed.) Static Analysis. LNCS, vol.\u00a06887, pp. 351\u2013368. Springer, Heidelberg (2011)"},{"key":"12_CR12","unstructured":"Falke, S., Merz, F., Sinz, C.: A theory of C-style memory allocation. In: Proc. SMT 2011, pp. 71\u201380 (2011)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A Decision Procedure for Bit-Vectors and Arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 519\u2013531. Springer, Heidelberg (2007)"},{"key":"12_CR14","unstructured":"Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The M\u00e4lardalen WCET benchmarks \u2013 past, present and future. In: Proc. WCET 2010, pp. 137\u2013147 (2010)"},{"issue":"3","key":"12_CR15","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1016\/j.tcs.2008.03.013","volume":"404","author":"F. Ivan\u010di\u0107","year":"2008","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. TCS\u00a0404(3), 256\u2013274 (2008)","journal-title":"TCS"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Kim, M., Kim, Y., Kim, H.: Unit testing of flash memory device driver through a SAT-based model checker. In: Proc. ASE 2008, 198\u2013207 (2008)","DOI":"10.1109\/ASE.2008.30"},{"key":"12_CR17","unstructured":"Kr\u00f6ning, D.: CBMC release 3.9 announcement on (December 19, 2010), cprovergooglegroups.com"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proc. CGO 2004, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-642-22110-1_49","volume-title":"Computer Aided Verification","author":"G. Li","year":"2011","unstructured":"Li, G., Ghosh, I., Rajan, S.: KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 609\u2013615. Springer, Heidelberg (2011)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-642-14203-1_29","volume-title":"Automated Reasoning","author":"F. Maric","year":"2010","unstructured":"Maric, F., Janicic, P.: URBiVA: Uniform Reduction to Bit-Vector Arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 346\u2013352. Springer, Heidelberg (2010)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-20398-5_21","volume-title":"NASA Formal Methods","author":"A. Milicevic","year":"2011","unstructured":"Milicevic, A., Kugler, H.: Model Checking using SMT and Theory of Lists. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 282\u2013297. Springer, Heidelberg (2011)"},{"key":"12_CR22","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.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"2","key":"12_CR23","first-page":"155","volume":"19","author":"H. Post","year":"2009","unstructured":"Post, H., Sinz, C., K\u00fcchlin, W.: Towards automatic software model checking of thousands of Linux modules\u2014A case study with Avinux. STVR\u00a019(2), 155\u2013172 (2009)","journal-title":"STVR"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A Scalable Memory Model for Low-Level Code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 290\u2013304. Springer, Heidelberg (2009)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Sinha, N.: Symbolic program analysis using term rewriting and generalization. In: Proc. FMCAD 2008, pp. 1\u20139 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.23"},{"key":"12_CR26","unstructured":"Sinz, C., Falke, S., Merz, F.: A precise memory model for low-level bounded model checking. In: Proc. SSV 2010 (2010)"},{"key":"12_CR27","series-title":"LNCS","first-page":"98","volume-title":"VSSTE 2012","author":"M. Vujosevic-Janicic","year":"2012","unstructured":"Vujosevic-Janicic, M., Kuncak, V.: Development and Evaluation of LAV: an SMT-Based Error Finding Platform. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSSTE 2012. LNCS, vol.\u00a07152, pp. 98\u2013113. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T08:20:22Z","timestamp":1742372422000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}