{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:06Z","timestamp":1767928506948,"version":"3.49.0"},"reference-count":50,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,3,31]],"date-time":"2025-03-31T00:00:00Z","timestamp":1743379200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,3,31]]},"DOI":"10.1109\/icst62969.2025.10988954","type":"proceedings-article","created":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T17:05:21Z","timestamp":1747760721000},"page":"441-452","source":"Crossref","is-referenced-by-count":1,"title":["Compiler Fuzzing in Continuous Integration: A Case Study on Dafny"],"prefix":"10.1109","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6750-6460","authenticated-orcid":false,"given":"Karnbongkot","family":"Boonriong","sequence":"first","affiliation":[{"name":"Imperial College London,London,UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-1304-0613","authenticated-orcid":false,"given":"Stefan","family":"Zetzsche","sequence":"additional","affiliation":[{"name":"Amazon Web Services,London,UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London,London,UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","article-title":"Amazon verified permissions","year":"2023"},{"key":"ref2","volume-title":"AWS cryptographicmaterial providers library","year":"2023"},{"key":"ref3","volume-title":"AWS encryption SDK for Dafny","year":"2023"},{"key":"ref4","volume-title":"AWS verified access","year":"2023"},{"key":"ref5","volume-title":"AWS re:Inforce 2024 - Proving thecorrectnessof AWS authorization (IAM401)","year":"2024"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/hase.2012.38"},{"key":"ref7","first-page":"364","article-title":"Boogie: A modular reusable verifier for object-oriented programs","volume-title":"Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005","volume":"4111","author":"Barnett","year":"2005"},{"key":"ref8","first-page":"571","article-title":"Formal and executable semantics of the Ethereum virtual machine in Dafny","volume-title":"Formal Methods - 25th International Symposium, FM 2023","volume":"14000","author":"Cassez","year":"2023"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884878"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/step.2003.18"},{"key":"ref11","volume-title":"C-Reduce","author":"Chen","year":"2024"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462173"},{"key":"ref13","first-page":"85","article-title":"Coverage-directed differential testing of JVM implementations","volume-title":"Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLD\/2016","author":"Chen","year":"2016"},{"key":"ref14","article-title":"CI Fuzz. efficient dynamic testing","volume-title":"Code Intelligence","year":"2024"},{"key":"ref15","article-title":"evm-dafny","volume-title":"Consensys","year":"2023"},{"key":"ref16","volume-title":"Dafny GitHub repository","author":"Project","year":"2023"},{"key":"ref17","first-page":"337","article-title":"Z3: an efficient SMT solver","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008","volume":"4963","author":"De Moura","year":"2008"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/icst57152.2023.00042"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3133917"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2896971.2896978"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/icst60714.2024.00044"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454092"},{"key":"ref23","volume-title":"Documentation for git-bisect","author":"Project","year":"2024"},{"key":"ref24","article-title":"OSS-Fuzz: Continuous fuzzing for open source software","volume-title":"Google","year":"2024"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3373087.3375310"},{"key":"ref27","volume-title":"How we built Cedar withautomated reasoning and differential testing","author":"Hicks","year":"2025"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534382"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/sbft59156.2023.00015"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"ref31","first-page":"1801","article-title":"Program reconditioning: Avoiding undefined behaviour when finding and reducing compiler bugs","volume-title":"Proc. ACM Program. Lang.","volume":"7","author":"Lecoeur","year":"2023"},{"key":"ref32","first-page":"348","article-title":"Dafny: An automatic program verifier for functional correctness","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16","volume":"6355","author":"Leino","year":"2010"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ms.2017.4121212"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"ref35","first-page":"29","article-title":"DeepCrash: deep metric learning for crash bucketing based on stack trace","volume-title":"Proceedings of the 6th International Workshop on Machine Learning Techniques for Software Quality Evaluation, MaLTeSQuE 2022","author":"Liu","year":"2022"},{"issue":"1","key":"ref36","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"McKeeman","year":"1998","journal-title":"Digital Technical Journal"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/3524842.3527951"},{"issue":"2","key":"ref39","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/s10664-021-10070-w","article-title":"Tracesim: An alignment method for computing stack trace similarity","volume":"27","author":"Rodrigues","year":"2022","journal-title":"Empir. Softw. Eng."},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/qrs.2017.35"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3604919"},{"key":"ref42","first-page":"849","article-title":"Finding compiler bugs via live code mutation","volume-title":"Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016","author":"Sun","year":"2016"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180236"},{"key":"ref44","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1109\/APSEC.2010.39","article-title":"An automatic testing approach for compiler based on metamorphic testing technique","volume-title":"17th Asia Pacific Software Engineering Conference, APSEC 2010","author":"Tao","year":"2010"},{"key":"ref45","volume-title":"SampCert version 1.0.0","author":"Tristan","year":"2024"},{"key":"ref46","volume-title":"fuzz-d GitHub repository","author":"Usher","year":"2023"},{"key":"ref47","article-title":"Verified BetrFS","volume-title":"VMware","year":"2024"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"ref49","article-title":"Towards a correct-by-construction FHE model","volume-title":"Cryptology ePrint Archive, Paper 2023\/281","author":"Yang","year":"2023"},{"key":"ref50","volume-title":"Dafny-VMC: a library for verified Monte Carlo algorithms","author":"Zetzsche","year":"2023"}],"event":{"name":"2025 IEEE Conference on Software Testing, Verification and Validation (ICST)","location":"Napoli, Italy","start":{"date-parts":[[2025,3,31]]},"end":{"date-parts":[[2025,4,4]]}},"container-title":["2025 IEEE Conference on Software Testing, Verification and Validation (ICST)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/10988917\/10988918\/10988954.pdf?arnumber=10988954","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T05:20:50Z","timestamp":1747804850000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10988954\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":50,"URL":"https:\/\/doi.org\/10.1109\/icst62969.2025.10988954","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]}}}