{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T04:11:28Z","timestamp":1746072688035,"version":"3.40.4"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031908996","type":"print"},{"value":"9783031909009","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the  category of Test-Comp 2025.<\/jats:p>","DOI":"10.1007\/978-3-031-90900-9_15","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:03Z","timestamp":1745988303000},"page":"281-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0416-3006","authenticated-orcid":false,"given":"Chenfeng","family":"Wei","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0986-4150","authenticated-orcid":false,"given":"Tong","family":"Wu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-4343","authenticated-orcid":false,"given":"Rafael Sa","family":"Menezes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3848-451X","authenticated-orcid":false,"given":"Fedor","family":"Shmarov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7683-8182","authenticated-orcid":false,"given":"Fatimah","family":"Aljaafari","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6169-6334","authenticated-orcid":false,"given":"Sangharatna","family":"Godboley","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5822-5435","authenticated-orcid":false,"given":"Kaled","family":"Alshmrany","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7608-2052","authenticated-orcid":false,"given":"Rosiane","family":"de Freitas","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Angeletti, D., Giunchiglia, E., Narizzano, M., Puddu, A., Sabina, S.: Automatic test generation for coverage analysis using cbmc. In: Computer Aided Systems Theory-EUROCAST 2009: 12th International Conference, Las Palmas de Gran Canaria, Spain, February 15-20, 2009, Revised Selected Papers 12. pp. 287\u2013294. Springer (2009)","DOI":"10.1007\/978-3-642-04772-5_38"},{"key":"15_CR2","unstructured":"Beyer, D.: Automatic testing of C programs: Test-Comp 2024. In: TBA. Springer (2024)"},{"key":"15_CR3","unstructured":"Beyer, D.: Advances in automatic software testing: Test-Comp 2025. In: Proc. FASE. Springer (2025)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Beyer, D., Dangl, M., Wendler, P.: Boosting k-induction with continuously-refined invariants. In: International Conference on Computer Aided Verification. pp. 622\u2013640. Springer (2015)","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Cho, C.Y., D\u2019Silva, V., Song, D.: Blitz: Compositional bounded model checking for real-world programs. In: 2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE). pp. 136\u2013146 (2013). https:\/\/doi.org\/10.1109\/ASE.2013.6693074","DOI":"10.1109\/ASE.2013.6693074"},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: Smt-based bounded model checking for embedded ansi-c software. IEEE Transactions on Software Engineering 38 (07 2009). https:\/\/doi.org\/10.1109\/TSE.2011.59","DOI":"10.1109\/TSE.2011.59"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Cordeiro, L., Fischer, B., Marques-Silva, J.: Smt-based bounded model checking for embedded ansi-c software. In: 2009 IEEE\/ACM International Conference on Automated Software Engineering. pp. 137\u2013148 (2009). https:\/\/doi.org\/10.1109\/ASE.2009.63","DOI":"10.1109\/ASE.2009.63"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Menezes, R.S., Cordeiro, L.C.: Esbmc 6.1: automated test case generation using bounded model checking. International Journal on Software Tools for Technology Transfer 23, 857\u2013861 (2021)","DOI":"10.1007\/s10009-020-00571-2"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: Esbmc 5.0: an industrial-strength c model checker. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering. pp. 888\u2013891 (2018)","DOI":"10.1145\/3238147.3240481"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis and transformation. In: International symposium on code generation and optimization. pp. 75\u201388. San Jose, CA, USA (Mar 2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Boolector 2.0. Journal on Satisfiability, Boolean Modeling and Computation 9(1), 53\u201358 (2014)","DOI":"10.3233\/SAT190101"},{"key":"15_CR13","unstructured":"Ramalho\u00a0Gadelha, M., et\u00a0al.: Scalable and precise verification based on k-induction, symbolic execution and floating-point theory. Ph.D. thesis, University of Southampton (2019)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90900-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:45:18Z","timestamp":1745988318000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90900-9_15"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031908996","9783031909009"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90900-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Fundamental Approaches to Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/fase\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}