{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:23:03Z","timestamp":1762298583653,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032095237"},{"type":"electronic","value":"9783032095244"}],"license":[{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T00:00:00Z","timestamp":1762300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-09524-4_1","type":"book-chapter","created":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T21:14:05Z","timestamp":1762290845000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["When You Have a\u00a0Fuzzer, Everything Looks Like a\u00a0Reachability Problem"],"prefix":"10.1007","author":[{"given":"Alastair F.","family":"Donaldson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3599-7264","authenticated-orcid":false,"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2477-2163","authenticated-orcid":false,"given":"Manuel","family":"Carrasco","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2313-7910","authenticated-orcid":false,"given":"Dan","family":"Iorga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7602-7707","authenticated-orcid":false,"given":"Daniel","family":"Liew","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,5]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Alglave, J., et al.: GPU concurrency: weak behaviours and programming assumptions. In: ASPLOS 2015. ACM (2015). https:\/\/doi.org\/10.1145\/2694344.2694391","DOI":"10.1145\/2694344.2694391"},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 1\u201374 (2014). https:\/\/doi.org\/10.1145\/2627752","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"1_CR3","doi-asserted-by":"publisher","first-page":"742","DOI":"10.1109\/TSE.2009.52","volume":"36","author":"S Ali","year":"2010","unstructured":"Ali, S., Briand, L.C., Hemmati, H., Panesar-Walawege, R.K.: A systematic review of the application and empirical investigation of search-based test case generation. IEEE Trans. Softw. Eng. 36(6), 742\u2013762 (2010). https:\/\/doi.org\/10.1109\/TSE.2009.52","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"1_CR4","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/S10703-023-00409-Y","volume":"63","author":"A Armstrong","year":"2024","unstructured":"Armstrong, A., Campbell, B., Simner, B., Pulte, C., Sewell, P.: Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). Formal Methods Syst. Des. 63(1), 110\u2013133 (2024). https:\/\/doi.org\/10.1007\/S10703-023-00409-Y","journal-title":"Formal Methods Syst. Des."},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-14295-6_11","volume-title":"Computer Aided Verification","author":"T Ball","year":"2010","unstructured":"Ball, T., Bounimova, E., Levin, V., Kumar, R., Lichtenberg, J.: The static driver verifier research platform. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 119\u2013122. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_11"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-662-46681-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Phan, A.-D., Fleckenstein, L.: $$\\nu $$z - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194\u2013199. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_14"},{"key":"1_CR7","unstructured":"Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI 2008. USENIX (2008)"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Carrasco, M., Cadar, C., Donaldson, A.F.: Scalable SMT sampling for floating-point formulas via coverage-guided fuzzing. In: ICST 2025. IEEE (2025). https:\/\/doi.org\/10.1109\/ICST62969.2025.10989031","DOI":"10.1109\/ICST62969.2025.10989031"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Carter, M., He, S., Whitaker, J., Rakamaric, Z., Emmi, M.: SMACK software verification toolchain. In: Dillon, L.K., Visser, W., Williams, L.A. (eds.) ICSE 2016 Companion Volume. ACM (2016). https:\/\/doi.org\/10.1145\/2889160.2889163","DOI":"10.1145\/2889160.2889163"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Delannoy, R., Meel, K.S.: On almost-uniform generation of SAT solutions: the power of 3-wise independent hashing. In: LICS 2022. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533338","DOI":"10.1145\/3531130.3533338"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Dutra, R., Bachrach, J., Sen, K.: SMTSampler: efficient stimulus generation from complex SMT constraints. In: ICCAD 2018. ACM (2018). https:\/\/doi.org\/10.1145\/3240765.3240848","DOI":"10.1145\/3240765.3240848"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Dutra, R., Laeufer, K., Bachrach, J., Sen, K.: Efficient sampling of SAT solutions for testing. In: ICSE 2018. ACM (2018). https:\/\/doi.org\/10.1145\/3180155.3180248","DOI":"10.1145\/3180155.3180248"},{"key":"1_CR14","unstructured":"Fioraldi, A., Maier, D., Ei\u00dffeldt, H., Heuse, M.: AFL++: combining incremental steps of fuzzing research. In: WOOT 2020. USENIX (2020)"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI 2005. ACM (2005). https:\/\/doi.org\/10.1145\/1065010.1065036","DOI":"10.1145\/1065010.1065036"},{"key":"1_CR16","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: NDSS 2008. The Internet Society (2008)"},{"key":"1_CR17","unstructured":"Google: ClusterFuzz (2025). https:\/\/github.com\/google\/clusterfuzz"},{"key":"1_CR18","unstructured":"Holland, J.: Adaptation in natural and artificial systems: an introductory analysis with applications to biology, control, and artificial intelligence. University of Michigan Press (1975)"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Huang, H., Yao, P., Wu, R., Shi, Q., Zhang, C.: Pangolin: incremental hybrid fuzzing with polyhedral path abstraction. In: S &P\u201920. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00063","DOI":"10.1109\/SP40000.2020.00063"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Iorga, D., Donaldson, A.F., Sorensen, T., Wickerson, J.: The semantics of shared memory in Intel CPU\/FPGA systems. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3485497","DOI":"10.1145\/3485497"},{"issue":"12","key":"1_CR21","doi-asserted-by":"publisher","first-page":"5084","DOI":"10.1109\/TSE.2023.3326056","volume":"49","author":"D Iorga","year":"2023","unstructured":"Iorga, D., Wickerson, J., Donaldson, A.F.: Simulating operational memory models using off-the-shelf program analysis tools. IEEE Trans. Softw. Eng. 49(12), 5084\u20135102 (2023). https:\/\/doi.org\/10.1109\/TSE.2023.3326056","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"9","key":"1_CR22","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","journal-title":"IEEE Trans. Comput."},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: LPAR 2010. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312\u2013327. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_26"},{"key":"1_CR25","unstructured":"LibFuzzer website (2025). http:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Liew, D., Cadar, C., Donaldson, A., Stinnett, J.R.: Just fuzz it: solving floating-point constraints using coverage-guided fuzzing. In: ESEC\/FSE 2019. ACM (2019). https:\/\/doi.org\/10.1145\/3338906.3338921","DOI":"10.1145\/3338906.3338921"},{"key":"1_CR27","doi-asserted-by":"publisher","unstructured":"Liew, D., Schemmel, D., Cadar, C., Donaldson, A., Z\u00e4hl, R., Wehrle, K.: Floating-point symbolic execution: a case study in N-version programming. In: ASE 2017. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115670","DOI":"10.1109\/ASE.2017.8115670"},{"issue":"12","key":"1_CR28","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/96267.96279","volume":"33","author":"BP Miller","year":"1990","unstructured":"Miller, B.P., Fredriksen, L., So, B.: An empirical study of the reliability of UNIX utilities. Commun. Assoc. Comput. Mach. (CACM) 33(12), 32\u201344 (1990). https:\/\/doi.org\/10.1145\/96267.96279","journal-title":"Commun. Assoc. Comput. Mach. (CACM)"},{"issue":"3","key":"1_CR29","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1609\/AIMAG.V28I3.2052","volume":"28","author":"Y Naveh","year":"2007","unstructured":"Naveh, Y., et al.: Constraint-based random stimuli generation for hardware verification. AI Mag. 28(3), 13\u201330 (2007). https:\/\/doi.org\/10.1609\/AIMAG.V28I3.2052","journal-title":"AI Mag."},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Plazar, Q., Acher, M., Perrouin, G., Devroey, X., Cordy, M.: Uniform sampling of SAT solutions for configurable systems: are we there yet? In: ICST 2019. IEEE (2019). https:\/\/doi.org\/10.1109\/ICST.2019.00032","DOI":"10.1109\/ICST.2019.00032"},{"key":"1_CR31","unstructured":"Poeplau, S., Francillon, A.: Symbolic execution with SymCC: don\u2019t interpret, compile! In: USENIX Security 2020. USENIX (2020)"},{"key":"1_CR32","doi-asserted-by":"publisher","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL), 19:1\u201319:29 (2018). https:\/\/doi.org\/10.1145\/3158107","DOI":"10.1145\/3158107"},{"key":"1_CR33","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: SMT 2010 (2010). http:\/\/www.cprover.org\/SMT-LIB-Float\/smt-fpa.pdf"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: PLDI 2011. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"1_CR35","unstructured":"Serebryany, K.: OSS-Fuzz \u2013 Google\u2019s continuous fuzzing service for open source software. In: Invited talk at USENIX Security 2017. USENIX (2017)"},{"key":"1_CR36","unstructured":"Zalewski, M.: Technical \u201cwhitepaper\u201d for afl-fuzz (2025). http:\/\/lcamtuf.coredump.cx\/afl\/technical_details.txt"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-09524-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:17:47Z","timestamp":1762298267000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-09524-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,5]]},"ISBN":["9783032095237","9783032095244"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-09524-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,5]]},"assertion":[{"value":"5 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Reachability Problems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"rp2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/rp25.software.imdea.org\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}