{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T11:29:52Z","timestamp":1763724592974,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,7,18]],"date-time":"2022-07-18T00:00:00Z","timestamp":1658102400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,7,18]]},"DOI":"10.1145\/3533767.3543289","type":"proceedings-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T14:28:50Z","timestamp":1657895330000},"page":"773-776","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC"],"prefix":"10.1145","author":[{"given":"Franz","family":"Brau\u00dfe","sequence":"first","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Fedor","family":"Shmarov","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Rafael","family":"Menezes","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Mikhail R.","family":"Gadelha","sequence":"additional","affiliation":[{"name":"Igalia, Brazil"}]},{"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Giles","family":"Reger","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[{"name":"University of Manchester, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,7,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_2_1","unstructured":"Armin Biere. 2009. Bounded Model Checking. In Handbook of Satisfiability. 457\u2013481. \t\t\t\t\t  Armin Biere. 2009. Bounded Model Checking. In Handbook of Satisfiability. 457\u2013481."},{"volume-title":"Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 341\u2013351","author":"Zhe","key":"e_1_3_2_1_3_1","unstructured":"Zhe Chen et al. 2019. Detecting memory errors at runtime with source-level instrumentation . In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 341\u2013351 . Zhe Chen et al. 2019. Detecting memory errors at runtime with source-level instrumentation. In Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis. 341\u2013351."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Edmund Clarke et al. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg Berlin Heidelberg. 168\u2013176. \t\t\t\t\t  Edmund Clarke et al. 2004. A Tool for Checking ANSI-C Programs. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg Berlin Heidelberg. 168\u2013176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304042"},{"volume-title":"Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering ASE. ACM, 888\u2013891","author":"Mikhail Y. R.","key":"e_1_3_2_1_7_1","unstructured":"Mikhail Y. R. Gadelha et al. 2018. ESBMC 5.0: an industrial-strength C model checker . In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering ASE. ACM, 888\u2013891 . Mikhail Y. R. Gadelha et al. 2018. ESBMC 5.0: an industrial-strength C model checker. In Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering ASE. ACM, 888\u2013891."},{"key":"e_1_3_2_1_8_1","volume-title":"LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In CGO.","author":"Chris Lattner","year":"2004","unstructured":"Chris Lattner et al. 2004 . LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In CGO. San Jose, CA, USA . 75\u201388. Chris Lattner et al. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis and Transformation. In CGO. San Jose, CA, USA. 75\u201388."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"volume-title":"Trends and Challenges in the Vulnerability Mitigation Landscape","author":"Matt Miller","key":"e_1_3_2_1_10_1","unstructured":"Matt Miller . 2019. Trends and Challenges in the Vulnerability Mitigation Landscape . USENIX Association , Santa Clara, CA . Matt Miller. 2019. Trends and Challenges in the Vulnerability Mitigation Landscape. USENIX Association, Santa Clara, CA."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1632"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1793"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542504"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837855.1806657"},{"volume-title":"In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 128\u2013139","author":"George C","key":"e_1_3_2_1_15_1","unstructured":"George C Necula et al. 2002. CCured: Type-safe retrofitting of legacy code . In In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 128\u2013139 . George C Necula et al. 2002. CCured: Type-safe retrofitting of legacy code. In In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 128\u2013139."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851830"},{"volume-title":"2012 USENIX Annual Tech. Conf. (ATC\u201912)","author":"Konstantin","key":"e_1_3_2_1_17_1","unstructured":"Konstantin Serebryany et al. 2012. AddressSanitizer: A fast address sanity checker . In 2012 USENIX Annual Tech. Conf. (ATC\u201912) . 309\u2013318. Konstantin Serebryany et al. 2012. AddressSanitizer: A fast address sanity checker. In 2012 USENIX Annual Tech. Conf. (ATC\u201912). 309\u2013318."},{"volume-title":"IEEE Cybersecurity Development Conference 2018 (SecDev). IEEE, 53\u201360","author":"David","key":"e_1_3_2_1_18_1","unstructured":"David Tarditi et al. 2018. Checked C: Making C Safe by Extension . In IEEE Cybersecurity Development Conference 2018 (SecDev). IEEE, 53\u201360 . David Tarditi et al. 2018. Checked C: Making C Safe by Extension. In IEEE Cybersecurity Development Conference 2018 (SecDev). IEEE, 53\u201360."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_3_2_1_20_1","volume-title":"Watson et al","author":"Robert N. M.","year":"2021","unstructured":"Robert N. M. Watson et al . 2021 . Assessing the Viability of an Open Source CHERI Desktop Software Ecosystem. Capabilities Limited . Robert N. M. Watson et al. 2021. Assessing the Viability of an Open Source CHERI Desktop Software Ecosystem. Capabilities Limited."},{"volume-title":"Cornucopia: Temporal Safety for CHERI Heaps. In 2020 IEEE Symposium on Security and Privacy (SP). 608\u2013625","author":"Nathaniel Wesley","key":"e_1_3_2_1_21_1","unstructured":"Nathaniel Wesley Filardo et al. 2020 . Cornucopia: Temporal Safety for CHERI Heaps. In 2020 IEEE Symposium on Security and Privacy (SP). 608\u2013625 . Nathaniel Wesley Filardo et al. 2020. Cornucopia: Temporal Safety for CHERI Heaps. In 2020 IEEE Symposium on Security and Privacy (SP). 608\u2013625."},{"volume-title":"ACM\/IEEE 41st Int. Symposium on Computer Architecture. 457\u2013468","author":"Jonathan","key":"e_1_3_2_1_22_1","unstructured":"Jonathan Woodruff et al. 2014. The CHERI capability model: Revisiting RISC in an age of risk . In ACM\/IEEE 41st Int. Symposium on Computer Architecture. 457\u2013468 . Jonathan Woodruff et al. 2014. The CHERI capability model: Revisiting RISC in an age of risk. In ACM\/IEEE 41st Int. Symposium on Computer Architecture. 457\u2013468."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2019.2914037"}],"event":{"name":"ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Virtual South Korea","acronym":"ISSTA '22"},"container-title":["Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3543289","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3533767.3543289","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:41Z","timestamp":1750272221000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3533767.3543289"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,18]]},"references-count":23,"alternative-id":["10.1145\/3533767.3543289","10.1145\/3533767"],"URL":"https:\/\/doi.org\/10.1145\/3533767.3543289","relation":{},"subject":[],"published":{"date-parts":[[2022,7,18]]},"assertion":[{"value":"2022-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}