{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:17:06Z","timestamp":1782875826311,"version":"3.54.5"},"reference-count":46,"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.10989031","type":"proceedings-article","created":{"date-parts":[[2025,5,20]],"date-time":"2025-05-20T17:05:21Z","timestamp":1747760721000},"page":"69-79","source":"Crossref","is-referenced-by-count":4,"title":["Scalable SMT Sampling for Floating-Point Formulas via Coverage-Guided Fuzzing"],"prefix":"10.1109","author":[{"given":"Manuel","family":"Carrasco","sequence":"first","affiliation":[{"name":"Imperial College London,London,United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London,London,United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London,London,United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","volume-title":"Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u2018 08)","author":"Cadar"},{"key":"ref2","article-title":"Symbolic execution with SymCC: Don\u2019t interpret, compile!","volume-title":"Proc. of the 29th USENIX Security Symposium (USENIX Security\u201920)","author":"Poeplau"},{"key":"ref3","article-title":"Automated whitebox fuzz testing","volume-title":"Proc. of the 15th Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00063"},{"key":"ref6","doi-asserted-by":"crossref","DOI":"10.1145\/3324884.3416629","article-title":"Legion: Best-first concolic testing","volume-title":"Proc. of the 35th IEEE International Conference on Automated Software Engineering (ASE\u201920)","author":"Liu"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/QRS54544.2021.00042"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-021-10102-5"},{"key":"ref9","volume-title":"Getting Involved","year":"2024"},{"key":"ref10","volume-title":"FAQ","year":"2025"},{"key":"ref11","volume-title":"Floating point - ISA and the IEEE standard (issue #326)","year":"2016"},{"key":"ref12","article-title":"Real Behavior of Floating Point Numbers","volume-title":"Proc. of the 15th International Workshop on Satisfiability Modulo Theories (SMT\u201917)","author":"Marre"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338921"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102235"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_11"},{"key":"ref20","volume-title":"Programming Z3","author":"Bomer","year":"2025"},{"key":"ref21","volume-title":"Programming Z3","year":"2025"},{"key":"ref22","volume-title":"Z3 very slow VC (issue #S23)","year":"2016"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351141"},{"key":"ref24","volume-title":"LibFuzzer website","year":"2022"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240848"},{"key":"ref26","article-title":"The SMT-LIB format: An initial proposal","volume-title":"Proc. of the Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR\u201903)","author":"Ranise"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"key":"ref28","volume-title":"Technical \u201cwhitepaper\u201d for afl-fuzz","author":"Zalewski","year":"2025"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115670"},{"key":"ref30","article-title":"IEEE Standard for Floating-Point Arithmetic","year":"2008","journal-title":"Institute of Electrical and Electronics Engineers, Standard"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_25"},{"key":"ref32","article-title":"Uniform solution sampling using a constraint solver as an oracle","volume-title":"Proc. of the 28th Conference on Uncertainty in Artificial Intelligence (UAI\u201907)","author":"Ermon"},{"key":"ref33","article-title":"vz - an optimizing SMT solver","volume-title":"Proc. of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2018 15","author":"Borner"},{"key":"ref34","volume-title":"SMTSampler: Efficient stimulus generation from complex SMT constraints","author":"Dutra","year":"2018"},{"key":"ref35","volume-title":"Model evaluation performance (issue #2341)","author":"Bueno","year":"2019"},{"key":"ref36","volume-title":"[artifact] SMTSampler\u2019s timeout calibration plots","author":"Carrasco","year":"2025"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1486"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2593097"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894251"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91265-9_15"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_31"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00071"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409748"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3100858"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2023.3326056"},{"key":"ref46","volume-title":"[artifact] Scalable SMT sampling for floating-point formulas via coverage-guided fuzzing","author":"Carrasco","year":"2025"}],"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\/10989031.pdf?arnumber=10989031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T05:10:54Z","timestamp":1747804254000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10989031\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,31]]},"references-count":46,"URL":"https:\/\/doi.org\/10.1109\/icst62969.2025.10989031","relation":{},"subject":[],"published":{"date-parts":[[2025,3,31]]}}}