{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T05:55:58Z","timestamp":1762322158530,"version":"3.41.0"},"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":1,"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"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London,London,United Kingdom"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London,London,United Kingdom"}]}],"member":"263","reference":[{"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":"ref1"},{"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":"ref2"},{"article-title":"Automated whitebox fuzz testing","volume-title":"Proc. of the 15th Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid","key":"ref3"},{"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"},{"volume-title":"Getting Involved","year":"2024","key":"ref9"},{"volume-title":"FAQ","year":"2025","key":"ref10"},{"volume-title":"Floating point - ISA and the IEEE standard (issue #326)","year":"2016","key":"ref11"},{"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":"ref12"},{"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"},{"volume-title":"Programming Z3","year":"2025","author":"Bomer","key":"ref20"},{"volume-title":"Programming Z3","year":"2025","key":"ref21"},{"volume-title":"Z3 very slow VC (issue #S23)","year":"2016","key":"ref22"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351141"},{"volume-title":"LibFuzzer website","year":"2022","key":"ref24"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240848"},{"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":"ref26"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180248"},{"volume-title":"Technical \u201cwhitepaper\u201d for afl-fuzz","year":"2025","author":"Zalewski","key":"ref28"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115670"},{"journal-title":"Institute of Electrical and Electronics Engineers, Standard","article-title":"IEEE Standard for Floating-Point Arithmetic","year":"2008","key":"ref30"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_25"},{"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":"ref32"},{"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":"ref33"},{"volume-title":"SMTSampler: Efficient stimulus generation from complex SMT constraints","year":"2018","author":"Dutra","key":"ref34"},{"volume-title":"Model evaluation performance (issue #2341)","year":"2019","author":"Bueno","key":"ref35"},{"volume-title":"[artifact] SMTSampler\u2019s timeout calibration plots","year":"2025","author":"Carrasco","key":"ref36"},{"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"},{"volume-title":"[artifact] Scalable SMT sampling for floating-point formulas via coverage-guided fuzzing","year":"2025","author":"Carrasco","key":"ref46"}],"event":{"name":"2025 IEEE Conference on Software Testing, Verification and Validation (ICST)","start":{"date-parts":[[2025,3,31]]},"location":"Napoli, Italy","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]]}}}