{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T14:57:13Z","timestamp":1770994633629,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T00:00:00Z","timestamp":1701302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101055412"],"award-info":[{"award-number":["101055412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,30]]},"DOI":"10.1145\/3611643.3616290","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:14:38Z","timestamp":1701386078000},"page":"1165-1176","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Engineering a Formally Verified Automated Bug Finder"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4439-7129","authenticated-orcid":false,"given":"Dominic","family":"Steinh\u00f6fel","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,11,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_29"},{"key":"e_1_3_2_2_2_1","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2026","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press. isbn:026202649X http:\/\/www.amazon.com\/Principles-Model-Checking-Christel-Baier\/dp\/026202649X"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.102.4"},{"key":"e_1_3_2_2_5_1","volume-title":"Formal Verification of a C Value Analysis Based on Abstract Interpretation","author":"Blazy Sandrine","unstructured":"Sandrine Blazy, Vincent Laporte, Andr\u00e9 Maroneze, and David Pichardie. 2013. Formal Verification of a C Value Analysis Based on Abstract Interpretation. In Static Analysis, Francesco Logozzo and Manuel F\u00e4hndrich (Eds.). Springer, 324\u2013344. isbn:978-3-642-38856-9"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468570"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2487274"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3433210.3453096"},{"key":"e_1_3_2_2_10_1","volume-title":"Proceedings of the 6th IFIP Congress","author":"Burstall Rod M.","year":"1974","unstructured":"Rod M. Burstall. 1974. Program Proving as Hand Simulation With a Little Induction. In Information Processing, Proceedings of the 6th IFIP Congress 1974, Jack L. Rosenfeld (Ed.). North-Holland, 308\u2013312."},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Arthur Correnson and Dominic Steinh\u00f6fel. 2023. Artifact for \"Engineering a Formally Verified Automated Bug Finder\". 10.5281\/zenodo.8269801","DOI":"10.5281\/zenodo.8269801"},{"key":"e_1_3_2_2_12_1","volume-title":"Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 238\u2013252","author":"Cousot P.","unstructured":"P. Cousot and R. Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 238\u2013252."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30942-8_6"},{"key":"e_1_3_2_2_14_1","volume-title":"On the cruelty of really teaching computing science","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra. 1988. On the cruelty of really teaching computing science. Center for American History, University of Texas at Austin. http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd10xx\/EWD1036.PDF EWD-1036."},{"key":"e_1_3_2_2_15_1","volume-title":"14th USENIX Workshop on Offensive Technologies, Yuval Yarom and Sarah Zennou (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi","author":"Fioraldi Andrea","year":"2020","unstructured":"Andrea Fioraldi, Dominik Christian Maier, Heiko Ei\u00dffeldt, and Marc Heuse. 2020. AFL++: Combining Incremental Steps of Fuzzing Research. In 14th USENIX Workshop on Offensive Technologies, Yuval Yarom and Sarah Zennou (Eds.). USENIX Association. https:\/\/www.usenix.org\/conference\/woot20\/presentation\/fioraldi"},{"key":"e_1_3_2_2_16_1","volume-title":"Types for Proofs and Programs","author":"Gim\u00e9nez Eduardo","unstructured":"Eduardo Gim\u00e9nez. 1996. An application of co-inductive types in Coq: Verification of the alternating bit protocol. In Types for Proofs and Programs, Stefano Berardi and Mario Coppo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 135\u2013152. isbn:978-3-540-70722-6"},{"key":"e_1_3_2_2_17_1","unstructured":"Eduardo Gim\u00e9nez and Pierre Cast\u00e9ran. 2007. A Tutorial on (Co-)Inductive Types in Coq. Available at https:\/\/www.labri.fr\/perso\/casteran\/RecTutorial.pdf."},{"key":"e_1_3_2_2_18_1","volume-title":"PLDI\u201905 Workshop on the Evaluation of Software Defect Detection Tools (BUGS\u201905)","author":"Godefroid Patrice","year":"2005","unstructured":"Patrice Godefroid. 2005. The Soundness of Bugs is What Matters (Position Statement). In PLDI\u201905 Workshop on the Evaluation of Software Defect Detection Tools (BUGS\u201905), Proceedings. https:\/\/patricegodefroid.github.io\/public_psfiles\/bugs2005.pdf"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_2_20_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201908). The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2008\/automated-whitebox-fuzz-testing\/"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115669"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547628"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90008-L"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_27_1","volume-title":"Reachable Coverage: Estimating Saturation in Fuzzing. In 45th IEEE\/ACM International Conference on Software Engineering (ICSE\u201923)","author":"Liyanage Danushka","year":"2023","unstructured":"Danushka Liyanage, Marcel B\u00f6hme, Chakkrit Tantithamthavorn, and Stephan Lipp. 2023. Reachable Coverage: Estimating Saturation in Fuzzing. In 45th IEEE\/ACM International Conference on Software Engineering (ICSE\u201923), Proceedings. ACM. https:\/\/mboehme.github.io\/paper\/ICSE23.Effectiveness.pdf to appear.."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2016.07.012"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_5"},{"key":"e_1_3_2_2_30_1","unstructured":"Rollbar. 2021. The State of Software Code Report. https:\/\/content.rollbar.com\/hubfs\/State-of-Software-Code-Report.pdf. Accessed: 2023-01-24."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2003.1201262"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"key":"e_1_3_2_2_33_1","volume-title":"Abstract Execution: Automatically Proving Infinitely Many Programs. Ph. D. Dissertation","author":"Steinh\u00f6fel Dominic","year":"2020","unstructured":"Dominic Steinh\u00f6fel. 2020. Abstract Execution: Automatically Proving Infinitely Many Programs. Ph. D. Dissertation. Darmstadt University of Technology, Germany. http:\/\/tuprints.ulb.tu-darmstadt.de\/8540\/"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(3:19)2015"}],"event":{"name":"ESEC\/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"San Francisco CA USA","acronym":"ESEC\/FSE '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616290","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611643.3616290","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:03Z","timestamp":1750178163000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616290"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,30]]},"references-count":34,"alternative-id":["10.1145\/3611643.3616290","10.1145\/3611643"],"URL":"https:\/\/doi.org\/10.1145\/3611643.3616290","relation":{},"subject":[],"published":{"date-parts":[[2023,11,30]]},"assertion":[{"value":"2023-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}