{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:01:44Z","timestamp":1776304904305,"version":"3.50.1"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572555","type":"print"},{"value":"9783031572562","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>ESBMC implements many state-of-the-art techniques that combine abstract interpretation and model checking. Here, we report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC now employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, and forward-backward contractors. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.<\/jats:p>","DOI":"10.1007\/978-3-031-57256-2_24","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"376-380","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["ESBMC v7.4: Harnessing the Power of Intervals"],"prefix":"10.1007","author":[{"given":"Rafael S\u00e1","family":"Menezes","sequence":"first","affiliation":[]},{"given":"Mohannad","family":"Aldughaim","sequence":"additional","affiliation":[]},{"given":"Bruno","family":"Farias","sequence":"additional","affiliation":[]},{"given":"Xianzhiyu","family":"Li","sequence":"additional","affiliation":[]},{"given":"Edoardo","family":"Manino","sequence":"additional","affiliation":[]},{"given":"Fedor","family":"Shmarov","sequence":"additional","affiliation":[]},{"given":"Kunjian","family":"Song","sequence":"additional","affiliation":[]},{"given":"Franz","family":"Brau\u00dfe","sequence":"additional","affiliation":[]},{"given":"Mikhail R.","family":"Gadelha","sequence":"additional","affiliation":[]},{"given":"Norbert","family":"Tihanyi","sequence":"additional","affiliation":[]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"M.\u00a0Aldughaim, K.\u00a0M. Alshmrany, M.\u00a0R. Gadelha, R.\u00a0de\u00a0Freitas, and L.\u00a0C. Cordeiro. FuSeBMC_IA: Interval analysis and methods for test case generation. In L.\u00a0Lambers and S.\u00a0Uchitel, editors, Fundamental Approaches to Software Engineering, pages 324\u2013329, Cham, 2023. Springer Nature Switzerland.","DOI":"10.1007\/978-3-031-30826-0_18"},{"key":"24_CR2","unstructured":"G.\u00a0Chabert and ibex team. ibex-lib, 2023. https:\/\/github.com\/ibex-team\/ibex-lib [Accessed: 19 December 2023]."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"E.\u00a0Clarke, D.\u00a0Kroening, and F.\u00a0Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems, pages 168\u2013176, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"L.\u00a0C. Cordeiro, B.\u00a0Fischer, and J.\u00a0Marques-Silva. SMT-based bounded model checking for embedded ANSI-C software. IEEE Transactions on Software Engineering, 38(4):957\u2013974, 2012.","DOI":"10.1109\/TSE.2011.59"},{"key":"24_CR5","unstructured":"P.\u00a0Cousot. Principles of Abstract Interpretation. MIT Press, 2021."},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"M.\u00a0Y.\u00a0R. Gadelha, F.\u00a0R. Monteiro, J.\u00a0Morse, L.\u00a0C. Cordeiro, B.\u00a0Fischer, and D.\u00a0A. Nicole. ESBMC 5.0: an industrial-strength C model checker. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering ASE, pages 888\u2013891. ACM, 2018.","DOI":"10.1145\/3238147.3240481"},{"key":"24_CR7","unstructured":"L.\u00a0Granvilliers. Revising hull and box consistency. Logic Programming, pages 230\u2013244, 1999."},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"E.\u00a0Hansen and G.\u00a0W. Walster. Global optimization using interval analysis: revised and expanded, volume 264. CRC Press, 2003.","DOI":"10.1201\/9780203026922"},{"key":"24_CR9","unstructured":"IEEE. IEEE standard for floating-point arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008), pages 1\u201384, 2019."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"L.\u00a0Jaulin, M.\u00a0Kieffer, O.\u00a0Didrit, and E.\u00a0Walter. Applied Interval Analysis. In Springer London, 2001.","DOI":"10.1007\/978-1-4471-0249-6"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"C.\u00a0Lattner and V.\u00a0Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In International symposium on code generation and optimization, pages 75\u201388, San Jose, CA, USA, Mar 2004.","DOI":"10.1109\/CGO.2004.1281665"},{"key":"24_CR12","unstructured":"E.\u00a0Manino, R.\u00a0S. Menezes, F.\u00a0Shmarov, and L.\u00a0C. Cordeiro. NeuroCodeBench: a plain C neural network benchmark for software verification, 2023."},{"key":"24_CR13","unstructured":"musl community. musl libc, 2023. https:\/\/musl.libc.org\/ [Accessed: 15 December 2023]."},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"M.\u00a0Mustafa, A.\u00a0Stancu, N.\u00a0Delanoue, and E.\u00a0Codres. Guaranteed SLAM\u2014An interval approach. Robotics and Autonomous Systems, 100:160\u2013170, 2018.","DOI":"10.1016\/j.robot.2017.11.009"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"A.\u00a0Neumaier. Interval methods for systems of equations, volume\u00a037. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511526473"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57256-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T17:22:16Z","timestamp":1731691336000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57256-2_24"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572555","9783031572562"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57256-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}