{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:50Z","timestamp":1776305090421,"version":"3.50.1"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030636173","type":"print"},{"value":"9783030636180","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-63618-0_5","type":"book-chapter","created":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T08:04:14Z","timestamp":1607155454000},"page":"68-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["BanditFuzz: A Reinforcement-Learning Based Performance Fuzzer for SMT Solvers"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Scott","sequence":"first","affiliation":[]},{"given":"Federico","family":"Mora","sequence":"additional","affiliation":[]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,12,6]]},"reference":[{"issue":"3","key":"5_CR1","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1109\/TR.2018.2805763","volume":"67","author":"D Appelt","year":"2018","unstructured":"Appelt, D., Nguyen, C.D., Panichella, A., Briand, L.C.: A machine-learning-driven evolutionary approach for testing web application firewalls. IEEE Trans. Reliab. 67(3), 733\u2013757 (2018)","journal-title":"IEEE Trans. Reliab."},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10009-010-0139-9","volume":"13","author":"C Artho","year":"2011","unstructured":"Artho, C.: Iterative delta debugging. Int. J. Softw. Tools Technol. Transf. 13(3), 223\u2013246 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"012001","DOI":"10.1088\/1742-6596\/341\/1\/012001","volume":"341","author":"S Baldwin","year":"2012","unstructured":"Baldwin, S.: Compute Canada: advancing computational research. J. Phys. Conf. Ser. 341, 012001 (2012). IOP Publishing","journal-title":"J. Phys. Conf. Ser."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14. http:\/\/www.cs.stanford.edu\/barrett\/pubs\/BCD+11.pdf"},{"key":"5_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: 2017 Formal Methods in Computer Aided Design (FMCAD), pp. 55\u201359. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-319-96142-2_6","volume-title":"Computer Aided Verification","author":"D Blotsky","year":"2018","unstructured":"Blotsky, D., Mora, F., Berzish, M., Zheng, Y., Kabir, I., Ganesh, V.: StringFuzz: a fuzzer for string solvers. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 45\u201351. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_6"},{"key":"5_CR8","unstructured":"Bobot-CEA, F., Chihani-CEA, Z., Iguernlala-OCamlPro, M., Marre-CEA, B.: FPA solver"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"B\u00f6ttinger, K., Godefroid, P., Singh, R.: Deep reinforcement fuzzing. arXiv preprint arXiv:1801.04589 (2018)","DOI":"10.1109\/SPW.2018.00026"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Brain, M., Tinelli, C., R\u00fcmmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: 2015 IEEE 22nd Symposium on Computer Arithmetic (ARITH), pp. 160\u2013167. IEEE (2015)","DOI":"10.1109\/ARITH.2015.26"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Brummayer, R., Biere, A.: Fuzzing and delta-debugging SMT solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pp. 1\u20135. ACM (2009)","DOI":"10.1145\/1670412.1670413"},{"key":"5_CR12","unstructured":"Bugariu, A., M\u00fcller, P.: Automatically testing string solvers. In: International Conference on Software Engineering (ICSE), 2020. ETH Zurich (2020)"},{"issue":"2","key":"5_CR13","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1145\/1455518.1455522","volume":"12","author":"C Cadar","year":"2008","unstructured":"Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: automatically generating inputs of death. ACM Trans. Inf. Syst. Secur. (TISSEC) 12(2), 10 (2008)","journal-title":"ACM Trans. Inf. Syst. Secur. (TISSEC)"},{"key":"5_CR14","unstructured":"Tinelli, C., Barrett, C., Fontaine, P.: Theory of unicode strings (draft) (2019). http:\/\/smtlib.cs.uiowa.edu\/theories-UnicodeStrings.shtml"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Cha, S.K., Woo, M., Brumley, D.: Program-adaptive mutational fuzzing. In: 2015 IEEE Symposium on Security and Privacy, pp. 725\u2013741. IEEE (2015)","DOI":"10.1109\/SP.2015.50"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"5_CR17","unstructured":"Committee, I.S., et al.: 754\u20132008 IEEE standard for floating-point arithmetic. IEEE Computer Society Std 2008, 517 (2008)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Peleg, H., Singh, R.: Learn&fuzz: machine learning for input fuzzing. In: Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, pp. 50\u201359. IEEE Press (2017)","DOI":"10.1109\/ASE.2017.8115618"},{"issue":"6","key":"5_CR20","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/1379022.1375616","volume":"43","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. ACM SIGPLAN Not. 43(6), 281\u2013292 (2008)","journal-title":"ACM SIGPLAN Not."},{"key":"5_CR21","doi-asserted-by":"publisher","DOI":"10.1201\/9781482276596","volume-title":"Handbook of Beta Distribution and Its Applications","author":"AK Gupta","year":"2004","unstructured":"Gupta, A.K., Nadarajah, S.: Handbook of Beta Distribution and Its Applications. CRC Press, Boca Raton (2004)"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Karamcheti, S., Mann, G., Rosenberg, D.: Adaptive grey-box fuzz-testing with Thompson sampling. In: Proceedings of the 11th ACM Workshop on Artificial Intelligence and Security, pp. 37\u201347. ACM (2018)","DOI":"10.1145\/3270101.3270108"},{"key":"5_CR23","unstructured":"Koza, J.R.: Genetic programming (1997)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-24690-6_28","volume-title":"Software Engineering and Formal Methods","author":"C Le Goues","year":"2011","unstructured":"Le Goues, C., Leino, K.R.M., Moskal, M.: The Boogie verification debugger (tool paper). In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 407\u2013414. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_28"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Padhye, R., Sen, K., Song, D.: PerfFuzz: automatically generating pathological inputs. In: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 254\u2013265 (2018)","DOI":"10.1145\/3213846.3213874"},{"issue":"3","key":"5_CR26","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/s10703-016-0247-6","volume":"48","author":"T Liang","year":"2016","unstructured":"Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Form. Methods Syst. Des. 48(3), 206\u2013234 (2016)","journal-title":"Form. Methods Syst. Des."},{"key":"5_CR27","unstructured":"Manes, V.J., et al.: Fuzzing: art, science, and engineering. arXiv preprint arXiv:1812.00140 (2018)"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Mansur, M.N., Christakis, M., W\u00fcstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. arXiv preprint arXiv:2004.05934 (2020)","DOI":"10.1145\/3368089.3409763"},{"key":"5_CR29","unstructured":"Heule, M., J\u00e4rvisalo, M., Suda, M.: SAT race 2019 (2019). http:\/\/sat-race-2019.ciirc.cvut.cz\/"},{"key":"5_CR30","unstructured":"Marre, B., Bobot, F., Chihani, Z.: Real behavior of floating point numbers. In: 15th International Workshop on Satisfiability Modulo Theories (2017)"},{"key":"5_CR31","unstructured":"Miller, C., Peterson, Z.N., et al.: Analysis of mutation and generation-based fuzzing. Technical report, Independent Security Evaluators (2007)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Misherghi, G., Su, Z.: HDD: hierarchical delta debugging. In: Proceedings of the 28th International Conference on Software Engineering, pp. 142\u2013151. ACM (2006)","DOI":"10.1145\/1134285.1134307"},{"key":"5_CR33","unstructured":"Niemetz, A., Biere, A.: ddSMT: a delta debugger for the SMT-LIB v2 format. In: Proceedings of the 11th International Workshop on Satisfiability Modulo Theories, SMT 2013), affiliated with the 16th International Conference on Theory and Applications of Satisfiability Testing, SAT 2013, Helsinki, Finland, 8\u20139 July 2013, pp. 36\u201345 (2013)"},{"key":"5_CR34","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Model-based API testing for SMT solvers. In: Brain, M., Hadarean, L. (eds.) Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017, affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, 24\u201328 July 2017, 10 pages (2017)"},{"key":"5_CR35","unstructured":"Patil, K., Kanade, A.: Greybox fuzzing as a contextual bandits problem. arXiv preprint arXiv:1806.03806 (2018)"},{"key":"5_CR36","first-page":"1","volume":"17","author":"S Rawat","year":"2017","unstructured":"Rawat, S., Jain, V., Kumar, A., Cojocar, L., Giuffrida, C., Bos, H.: VUzzer: application-aware evolutionary fuzzing. NDSS 17, 1\u201314 (2017)","journal-title":"NDSS"},{"key":"5_CR37","unstructured":"Rebert, A., et al.: Optimizing seed selection for fuzzing. In: USENIX Security Symposium, pp. 861\u2013875 (2014)"},{"key":"5_CR38","unstructured":"R\u00fcmmer, P., Wahl, T.: An SMT-LIB theory of binary floating-point arithmetic. In: International Workshop on Satisfiability Modulo Theories (SMT), p. 151 (2010)"},{"key":"5_CR39","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"2016","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Pearson Education Limited, Malaysia (2016)"},{"issue":"1","key":"5_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/2200000070","volume":"11","author":"DJ Russo","year":"2018","unstructured":"Russo, D.J., Van Roy, B., Kazerouni, A., Osband, I., Wen, Z., et al.: A tutorial on Thompson sampling. Found. Trends\u00ae Mach. Learn. 11(1), 1\u201396 (2018)","journal-title":"Found. Trends\u00ae Mach. Learn."},{"key":"5_CR41","unstructured":"Seagle Jr., R.L.: A framework for file format fuzzing with genetic algorithms (2012)"},{"key":"5_CR42","doi-asserted-by":"publisher","DOI":"10.1002\/9781118557426","volume-title":"Markov Decision Processes in Artificial Intelligence","author":"O Sigaud","year":"2013","unstructured":"Sigaud, O., Buffet, O.: Markov Decision Processes in Artificial Intelligence. Wiley, New York (2013)"},{"key":"5_CR43","volume-title":"Fuzzing: Brute Force Vulnerability Discovery","author":"M Sutton","year":"2007","unstructured":"Sutton, M., Greene, A., Amini, P.: Fuzzing: Brute Force Vulnerability Discovery. Pearson Education, Upper Saddle River (2007)"},{"key":"5_CR44","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (2018)"},{"key":"5_CR45","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G., et al.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (1998)"},{"issue":"1","key":"5_CR46","first-page":"1","volume":"4","author":"C Szepesv\u00e1ri","year":"2010","unstructured":"Szepesv\u00e1ri, C.: Algorithms for reinforcement learning. Synt. Lect. Artif. Intell. Mach. Learn. 4(1), 1\u2013103 (2010)","journal-title":"Synt. Lect. Artif. Intell. Mach. Learn."},{"key":"5_CR47","volume-title":"Fuzzing for Software Security Testing and Quality Assurance","author":"A Takanen","year":"2008","unstructured":"Takanen, A., Demott, J.D., Miller, C.: Fuzzing for Software Security Testing and Quality Assurance. Artech House, Norwood (2008)"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Woo, M., Cha, S.K., Gottlieb, S., Brumley, D.: Scheduling black-box mutational fuzzing. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, pp. 511\u2013522. ACM (2013)","DOI":"10.1145\/2508859.2516736"},{"key":"5_CR49","unstructured":"Zalewski, M.: American fuzzy lop (2015)"},{"issue":"2","key":"5_CR50","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63618-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T00:45:56Z","timestamp":1619225156000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63618-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030636173","9783030636180"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63618-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"6 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE20\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"57% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to COVID-19 pandemic the conference was held virtually","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}