{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T21:03:43Z","timestamp":1773522223088,"version":"3.50.1"},"reference-count":135,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,3,20]],"date-time":"2024-03-20T00:00:00Z","timestamp":1710892800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["1901136"],"award-info":[{"award-number":["1901136"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2024,3,31]]},"abstract":"<jats:p>\n            Testing to detect semantic bugs is essential, especially for critical systems. Coverage-guided fuzzing (CGF) and runtime assertion checking (RAC) are two well-known approaches for detecting semantic bugs. CGF aims to generate test inputs with high code coverage. However, while CGF tools can be equipped with sanitizers to detect a fixed set of semantic bugs, they can otherwise only detect bugs that lead to a crash. Thus, the first problem we address is how to help fuzzers detect previously unknown semantic bugs that do not lead to a crash. Moreover, a CGF tool may not necessarily cover all branches with valid inputs, although invalid inputs are useless for detecting semantic bugs. So, the second problem is how to guide a fuzzer to maximize coverage using only valid inputs. However, RAC monitors the expected behavior of a program dynamically and can only detect a semantic bug when a valid test input shows that the program does not satisfy its specification. Thus, the third problem is how to provide high-quality test inputs for a RAC that can trigger potential bugs. The combination of a CGF tool and RAC solves these problems and can cover branches with valid inputs and detect semantic bugs effectively. Our study uses RAC to guarantee that only valid inputs reach the program under test using the program\u2019s specified preconditions, and it also uses RAC to detect semantic bugs using specified postconditions. A prototype tool was developed for this study, named JMLKelinci+. Our results show that combining a CGF tool with RAC will lead to executing the program under test only with valid inputs and that this technique can effectively detect semantic bugs. Also, this idea improves the feedback given to a CGF tool, enabling it to cover all branches faster in programs with non-trivial preconditions.\n            <jats:xref ref-type=\"fn\">\n              <jats:sup>1<\/jats:sup>\n            <\/jats:xref>\n          <\/jats:p>","DOI":"10.1145\/3607538","type":"journal-article","created":{"date-parts":[[2023,8,5]],"date-time":"2023-08-05T09:12:33Z","timestamp":1691226753000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["JMLKelinci+: Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking"],"prefix":"10.1145","volume":"36","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9031-5599","authenticated-orcid":false,"given":"Amirfarhad","family":"Nilizadeh","sequence":"first","affiliation":[{"name":"University of Central Florida, Orlando, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3271-3921","authenticated-orcid":false,"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[{"name":"University of Central Florida, Orlando, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5579-6961","authenticated-orcid":false,"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University\/NASA Ames Research Center, Moffett Field, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9318-8027","authenticated-orcid":false,"given":"Yannic","family":"Noller","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-49812-6","article-title":"Deductive software verification-the key book","author":"Ahrendt Wolfgang","year":"2016","unstructured":"Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H\u00e4hnle, Peter H. Schmitt, and Mattias Ulbrich. 2016. Deductive software verification-the key book. In Lecture Notes in Computer Science (2016).","journal-title":"Lecture Notes in Computer Science"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.11.007"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/11836810_25"},{"key":"e_1_3_3_8_2","first-page":"104","volume-title":"International Symposium on Leveraging Applications of Formal Methods","author":"Bardin S\u00e9bastien","year":"2018","unstructured":"S\u00e9bastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentr\u00e9, and Nicky Williams. 2018. Test case generation with PathCrawler\/LTest: How to automate an industrial testing process. In International Symposium on Leveraging Applications of Formal Methods. Springer, 104\u2013120."},{"key":"e_1_3_3_9_2","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/11513988_16","volume-title":"International Conference on Computer Aided Verification","author":"Barner Sharon","year":"2005","unstructured":"Sharon Barner, Ziv Glazberg, and Ishai Rabinovitz. 2005. Wolf\u2013bug hunter for concurrent software using formal methods. In International Conference on Computer Aided Verification. Springer, 153\u2013157."},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/1808999"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"e_1_3_3_12_2","first-page":"291","article-title":"Address obfuscation: An efficient approach to combat a broad range of memory error exploits","author":"Bhatkar Sandeep","year":"2003","unstructured":"Sandeep Bhatkar, Daniel C. DuVarney, and Ron Sekar. 2003. Address obfuscation: An efficient approach to combat a broad range of memory error exploits. In Proceedings of the USENIX Security Symposium, 291\u2013301.","journal-title":"Proceedings of the USENIX Security Symposium"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.375178"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/566171.566191"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"key":"e_1_3_3_16_2","first-page":"16","volume-title":"International Workshop on Formal Approaches to Software Testing","author":"Brucker Achim D.","year":"2004","unstructured":"Achim D. Brucker and Burkhart Wolff. 2004. Symbolic test case generation for primitive recursive functions. In International Workshop on Formal Approaches to Software Testing. Springer, 16\u201332."},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-662-46675-9_6","volume-title":"International Conference on Fundamental Approaches to Software Engineering","author":"B\u00fcrdek Johannes","year":"2015","unstructured":"Johannes B\u00fcrdek, Malte Lochau, Stefan Bauregger, Andreas Holzer, Alexander Von Rhein, Sven Apel, and Dirk Beyer. 2015. Facilitating reuse in multi-goal test-suite generation for software product lines. In International Conference on Fundamental Approaches to Software Engineering. Springer, 84\u201399."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_3_20_2","first-page":"2","volume-title":"International Conference on Technical Formal Methods","author":"Catano Nestor","year":"2009","unstructured":"Nestor Catano and Camilo Rueda. 2009. Teaching formal methods for the unconquered territory. In International Conference on Technical Formal Methods. Springer, 2\u201319."},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cosrev.2019.01.002"},{"key":"e_1_3_3_23_2","series-title":"Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO\u201905),","first-page":"342","author":"Chalin Patrice","year":"2006","unstructured":"Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. 2006. Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO\u201905),Lecture Notes in Computer Science, Vol. 4111. Springer-Verlag, Berlin, 342\u2013363. https:\/\/tinyurl.com\/3z2vk55n"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213008003947"},{"key":"e_1_3_3_25_2","first-page":"21","volume-title":"Proceedings of the IEEE Workshop on Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE\u201917)","author":"Chappelly Timothy","year":"2017","unstructured":"Timothy Chappelly, Cristina Cifuentes, Padmanabhan Krishnan, and Shlomo Gevay. 2017. Machine learning for finding bugs: An initial report. In Proceedings of the IEEE Workshop on Machine Learning Techniques for Software Quality Evaluation (MaLTeSQuE\u201917). IEEE, 21\u201326."},{"key":"e_1_3_3_26_2","first-page":"171","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS\u201904)","volume":"4","author":"Chen Hao","year":"2004","unstructured":"Hao Chen, Drew Dean, and David A. Wagner. 2004. Model checking one million lines of C code. In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201904), Vol. 4. 171\u2013185."},{"key":"e_1_3_3_27_2","first-page":"322","volume-title":"Proceedings of the International Conference on Software Engineering Research and Practice (SERP\u201902)","author":"Cheon Yoonsik","year":"2002","unstructured":"Yoonsik Cheon and Gary T. Leavens. 2002. A runtime assertion checker for the java modeling language (JML). In Proceedings of the International Conference on Software Engineering Research and Practice (SERP\u201902), Hamid R. Arabnia and Youngsong Mun (Eds.). CSREA Press, 322\u2013328."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/646159.680018"},{"key":"e_1_3_3_29_2","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"International Conference on Computer Aided Verification","author":"Chudnov Andrey","year":"2018","unstructured":"Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacC\u00e1rthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, et\u00a0al. 2018. Continuous formal verification of Amazon s2n. In International Conference on Computer Aided Verification. Springer, 430\u2013446."},{"key":"e_1_3_3_30_2","first-page":"268","volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming","author":"Claessen Koen","year":"2000","unstructured":"Koen Claessen and John Hughes. 2000. QuickCheck: A lightweight tool for random testing of haskell programs. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming. 268\u2013279."},{"key":"e_1_3_3_31_2","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-540-39910-0_9","volume-title":"Verification: Theory and Practice","author":"Clarke Edmund","year":"2003","unstructured":"Edmund Clarke and Helmut Veith. 2003. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice. Springer, 208\u2013224."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127900"},{"key":"e_1_3_3_33_2","volume-title":"Model Checking","author":"Jr Edmund M. Clarke","year":"2018","unstructured":"Edmund M. Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking. MIT Press."},{"issue":"6","key":"e_1_3_3_34_2","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/s10009-010-0138-x","article-title":"Improved usability and performance of SMT solvers for debugging specifications","volume":"12","author":"Cok David R.","year":"2010","unstructured":"David R. Cok. 2010. Improved usability and performance of SMT solvers for debugging specifications. Int. J. Softw. Tools Technol. Transf. 12, 6 (2010), 467\u2013481.","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"e_1_3_3_35_2","first-page":"472","volume-title":"NASA Formal Methods Symposium","author":"Cok David R.","year":"2011","unstructured":"David R. Cok. 2011. OpenJML: JML for Java 7 by extending OpenJDK. In NASA Formal Methods Symposium. Springer, 472\u2013479."},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468417"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464971.3468417"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2948707"},{"key":"e_1_3_3_39_2","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-319-96145-3_3","volume-title":"International Conference on Computer Aided Verification","author":"Cook Byron","year":"2018","unstructured":"Byron Cook. 2018. Formal reasoning about the security of amazon web services. In International Conference on Computer Aided Verification. Springer, 38\u201347."},{"key":"e_1_3_3_40_2","first-page":"2123","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer and Communications Security","author":"Corina Jake","year":"2017","unstructured":"Jake Corina, Aravind Machiry, Christopher Salls, Yan Shoshitaishvili, Shuang Hao, Christopher Kruegel, and Giovanni Vigna. 2017. DIFUZE: Interface aware fuzzing for kernel drivers. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. 2123\u20132138."},{"key":"e_1_3_3_41_2","first-page":"313","volume-title":"European Symposium on Research in Computer Security","author":"Decker Christian","year":"2014","unstructured":"Christian Decker and Roger Wattenhofer. 2014. Bitcoin transaction malleability and MtGox. In European Symposium on Research in Computer Security. Springer, 313\u2013326."},{"issue":"4","key":"e_1_3_3_42_2","first-page":"23","article-title":"Acceptance of formal methods: Lessons from hardware design","volume":"29","author":"Dill David L.","year":"1996","unstructured":"David L. Dill and John Rushby. 1996. Acceptance of formal methods: Lessons from hardware design. IEEE Comput. 29, 4 (1996), 23\u201324.","journal-title":"IEEE Comput."},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2663716.2663755"},{"key":"e_1_3_3_44_2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/978-3-030-59762-7_8","volume-title":"International Symposium on Search Based Software Engineering","author":"Eberlein Martin","year":"2020","unstructured":"Martin Eberlein, Yannic Noller, Thomas Vogel, and Lars Grunske. 2020. Evolutionary grammar-based fuzzing. In International Symposium on Search Based Software Engineering. Springer, 105\u2013120."},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/263244.263267"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025179"},{"key":"e_1_3_3_47_2","first-page":"362","volume-title":"Proceedings of the IEEE 6th International Conference on Software Testing, Verification and Validation","author":"Fraser Gordon","year":"2013","unstructured":"Gordon Fraser and Andrea Arcuri. 2013. EvoSuite: On the challenges of test case generation in the real world. In Proceedings of the IEEE 6th International Conference on Software Testing, Verification and Validation. IEEE, 362\u2013369."},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2685612"},{"key":"e_1_3_3_49_2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/1806799.1806835","volume-title":"Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering-Volume 1","author":"Gligoric Milos","year":"2010","unstructured":"Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor Kuncak, and Darko Marinov. 2010. Test generation through programming in UDITA. In Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering-Volume 1. 225\u2013234."},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375607"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155573"},{"key":"e_1_3_3_53_2","unstructured":"Google et\u00a0al. [n.d.]. google\/syzkaller. Retrieved May 5 2023 from https:\/\/github.com\/google\/syzkaller"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_3_3_55_2","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/978-3-319-17524-9_15","volume-title":"NASA Formal Methods Symposium","author":"Groce Alex","year":"2015","unstructured":"Alex Groce and Jervis Pinto. 2015. A little language for testing. In NASA Formal Methods Symposium. Springer, 204\u2013218."},{"key":"e_1_3_3_56_2","first-page":"414","volume-title":"Proceedings of the International Symposium on Software Testing and Analysis","author":"Groce Alex","year":"2015","unstructured":"Alex Groce, Jervis Pinto, Pooria Azimi, and Pranjal Mittal. 2015. TSTL: A language and tool for testing. In Proceedings of the International Symposium on Software Testing and Analysis. 414\u2013417."},{"key":"e_1_3_3_57_2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"International SPIN Workshop on Model Checking of Software","author":"Groce Alex","year":"2003","unstructured":"Alex Groce and Willem Visser. 2003. What went wrong: Explaining counterexamples. In International SPIN Workshop on Model Checking of Software. Springer, 121\u2013136."},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.57887"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0143-6"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3278186.3278193"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107233"},{"key":"e_1_3_3_63_2","unstructured":"Marc R. Hoffmann Evgeny Mandrikov and Mirko Friedenhagen. [n.d.]. Java Code Coverage for Eclipse. Retrieved May 5 2023 from https:\/\/www.eclemma.org\/jacoco\/"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0445-y"},{"key":"e_1_3_3_65_2","unstructured":"JavaJML [n.d.]. Java-JML. Retrieved May 5 2023 from https:\/\/github.com\/Amirfarhad-Nilizadeh\/Java-JML"},{"key":"e_1_3_3_66_2","first-page":"249","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201920)","author":"Jeon Yuseok","year":"2020","unstructured":"Yuseok Jeon, WookHyun Han, Nathan Burow, and Mathias Payer. 2020. FuZZan: Efficient sanitizer metadata design for fuzzing. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201920). 249\u2013263."},{"key":"e_1_3_3_67_2","first-page":"275","volume-title":"Proceedings of the IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW\u201919)","author":"Jitsunari Yuma","year":"2019","unstructured":"Yuma Jitsunari and Yoshitaka Arahori. 2019. Coverage-guided learning-assisted grammar-based fuzzing. In Proceedings of the IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW\u201919). IEEE, 275\u2013280."},{"key":"e_1_3_3_68_2","first-page":"323","volume-title":"Proceedings of the IEEE 7th International Conference on Software Testing, Verification and Validation","author":"Johansson William","year":"2014","unstructured":"William Johansson, Martin Svensson, Ulf E. Larson, Magnus Almgren, and Vincenzo Gulisano. 2014. T-Fuzz: Model-based fuzzing for robustness testing of telecommunication protocols. In Proceedings of the IEEE 7th International Conference on Software Testing, Verification and Validation. IEEE, 323\u2013332."},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2628055"},{"key":"e_1_3_3_70_2","first-page":"2511","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer and Communications Security","author":"Kersten Rody","year":"2017","unstructured":"Rody Kersten, Kasper Luckow, and Corina S P\u0103s\u0103reanu. 2017. POSTER: AFL-based fuzzing for java with kelinci. In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security. 2511\u20132513."},{"key":"e_1_3_3_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_3_72_2","first-page":"244","volume-title":"International Symposium on Trustworthy Global Computing","author":"Kiniry Joseph R.","year":"2006","unstructured":"Joseph R. Kiniry, Alan E. Morkan, Dermot Cochran, Fintan Fairmichael, Patrice Chalin, Martijn Oostdijk, and Engelbert Hubbers. 2006. The KOA remote voting system: A summary of work to date. In International Symposium on Trustworthy Global Computing. Springer, 244\u2013262."},{"key":"e_1_3_3_73_2","first-page":"310","volume-title":"International Conference on Runtime Verification","author":"Kosmatov Nikolai","year":"2020","unstructured":"Nikolai Kosmatov, Fonenantsoa Maurica, and Julien Signoles. 2020. Efficient runtime assertion checking for properties over mathematical numbers. In International Conference on Runtime Verification. Springer, 310\u2013322."},{"key":"e_1_3_3_74_2","unstructured":"Gary Kwong Jesse Ruderman and Antonine Carette. [n.d.]. MozillaSecurity\/funfuzz. Retrieved May 5 2023 frp https:\/\/github.com\/MozillaSecurity\/funfuzz"},{"key":"e_1_3_3_75_2","first-page":"1","article-title":"Coverage guided, property based testing","author":"Lampropoulos Leonidas","year":"2019","unstructured":"Leonidas Lampropoulos, Michael Hicks, and Benjamin C Pierce. 2019. Coverage guided, property based testing. In Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201919), 1\u201329.","journal-title":"Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201919)"},{"key":"e_1_3_3_76_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00064"},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3364452.3364455"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127884"},{"key":"e_1_3_3_80_2","unstructured":"Gary T. Leavens and Yoonsik Cheon. 2006. Design by Contract with JML. Retrieved from https:\/\/www.cs.ucf.edu\/leavens\/JML\/\/jmldbc.pdf"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_3_3_82_2","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-031-08166-8_15","volume-title":"The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday","author":"Leavens Gary T.","year":"2022","unstructured":"Gary T. Leavens, David R. Cok, and Amirfarhad Nilizadeh. 2022. Further lessons from the JML project. In The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday. Springer, 313\u2013349."},{"key":"e_1_3_3_83_2","unstructured":"Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman et\u00a0al. 2008. JML Reference Manual."},{"key":"e_1_3_3_84_2","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/367845.367996","volume-title":"Addendum to the 2000 Proceedings of the Conference on Object-oriented Programming, Systems, Languages, and Applications (Addendum)","author":"Leavens Gary T.","year":"2000","unstructured":"Gary T. Leavens, Clyde Ruby, K. Rustan M. Leino, Erik Poll, and Bart Jacobs. 2000. JML (poster session) notations and tools supporting detailed design in Java. In Addendum to the 2000 Proceedings of the Conference on Object-oriented Programming, Systems, Languages, and Applications (Addendum). 105\u2013106."},{"key":"e_1_3_3_85_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"e_1_3_3_86_2","doi-asserted-by":"publisher","DOI":"10.1186\/s42400-018-0002-y"},{"key":"e_1_3_3_87_2","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2018.2834476"},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50995-8_6"},{"key":"e_1_3_3_89_2","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1145\/3395351.3399360","volume-title":"Proceedings of the 13th ACM Conference on Security and Privacy in Wireless and Mobile Networks","author":"Maier Dominik","year":"2020","unstructured":"Dominik Maier, Lukas Seidel, and Shinjo Park. 2020. Basesafe: Baseband sanitized fuzzing through emulation. In Proceedings of the 13th ACM Conference on Security and Privacy in Wireless and Mobile Networks. 122\u2013132."},{"key":"e_1_3_3_90_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.asoc.2014.11.023"},{"key":"e_1_3_3_91_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180191"},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-016-9470-4"},{"key":"e_1_3_3_93_2","first-page":"447","volume-title":"Proceedings of the IEEE 6th International Conference on Software Testing, Verification and Validation","author":"Meinke Karl","year":"2013","unstructured":"Karl Meinke and Muddassar A Sindhu. 2013. LBTest: A learning-based testing tool for reactive systems. In Proceedings of the IEEE 6th International Conference on Software Testing, Verification and Validation. IEEE, 447\u2013454."},{"key":"e_1_3_3_94_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_3_95_2","first-page":"771","volume-title":"Proceedings of the 29th International Conference on Software Engineering (ICSE\u201907)","author":"Milicevic Aleksandar","year":"2007","unstructured":"Aleksandar Milicevic, Sasa Misailovic, Darko Marinov, and Sarfraz Khurshid. 2007. Korat: A tool for generating structurally complex test inputs. In Proceedings of the 29th International Conference on Software Engineering (ICSE\u201907). IEEE, 771\u2013774."},{"key":"e_1_3_3_96_2","first-page":"787","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (SP\u201919)","author":"Nagy Stefan","year":"2019","unstructured":"Stefan Nagy and Matthew Hicks. 2019. Full-speed fuzzing: Reducing fuzzing overhead through coverage-guided tracing. In Proceedings of the IEEE Symposium on Security and Privacy (SP\u201919). IEEE, 787\u2013802."},{"key":"e_1_3_3_97_2","doi-asserted-by":"publisher","DOI":"10.1002\/smr.1789"},{"key":"e_1_3_3_98_2","unstructured":"Amirfarhad Nilizadeh. [n.d.]. JMLKelinciPlus. Retrieved May 5 2023 https:\/\/zenodo.org\/record\/7458704#.Y6CmT1FOk2w"},{"key":"e_1_3_3_99_2","volume-title":"Test Overfitting: Challenges, Approaches, and Measurements","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh. 2021. Test Overfitting: Challenges, Approaches, and Measurements. Technical Report. University of Central Florida, Computer Science."},{"key":"e_1_3_3_100_2","first-page":"480","volume-title":"Proceedings of the IEEE Conference on Software Testing, Verification and Validation (ICST\u201922)","author":"Nilizadeh Amirfarhad","year":"2022","unstructured":"Amirfarhad Nilizadeh. 2022. Automated program repair and test overfitting: Measurements and approaches using formal methods. In Proceedings of the IEEE Conference on Software Testing, Verification and Validation (ICST\u201922). IEEE, 480\u2013482."},{"key":"e_1_3_3_101_2","doi-asserted-by":"publisher","DOI":"10.1145\/3524482.3527656"},{"key":"e_1_3_3_102_2","first-page":"208","volume-title":"Proceedings of the IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE\u201921)","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh, Marlon Calvo, Gary T. Leavens, and Xuan-Bach D. Le. 2021. More reliable test suites for dynamic APR by using counterexamples. In Proceedings of the IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE\u201921). IEEE, 208\u2013219."},{"key":"e_1_3_3_103_2","doi-asserted-by":"publisher","DOI":"10.1145\/3524459.3527346"},{"key":"e_1_3_3_104_2","first-page":"229","volume-title":"Proceeding of the 14th IEEE Conference on Software Testing, Verification and Validation (ICST\u201921)","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh, Gary T. Leavens, Xuan-Bach D. Le, Corina S. P\u0103s\u0103reanu, and David R. Cok. 2021. Exploring true test overfitting in dynamic automated program repair using formal methods. In Proceeding of the 14th IEEE Conference on Software Testing, Verification and Validation (ICST\u201921). IEEE, Los Alamitos, CA, 229\u2013240."},{"key":"e_1_3_3_105_2","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-030-79379-1_5","volume-title":"Tests and Proofs","author":"Nilizadeh Amirfarhad","year":"2021","unstructured":"Amirfarhad Nilizadeh, Gary T. Leavens, and Corina S. P\u0103s\u0103reanu. 2021. Using a guided fuzzer and preconditions to achieve branch coverage with valid inputs. In Tests and Proofs, Fr\u00e9d\u00e9ric Loulergue and Franz Wotawa (Eds.). Springer International Publishing, Cham, 72\u201384."},{"key":"e_1_3_3_106_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00034"},{"key":"e_1_3_3_107_2","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213868"},{"key":"e_1_3_3_108_2","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380363"},{"key":"e_1_3_3_109_2","first-page":"2289","volume-title":"Proceedings of the 29th USENIX Security Symposium (USENIX Security\u201920)","author":"\u00d6sterlund Sebastian","year":"2020","unstructured":"Sebastian \u00d6sterlund, Kaveh Razavi, Herbert Bos, and Cristiano Giuffrida. 2020. Parmesan: Sanitizer-guided greybox fuzzing. In Proceedings of the 29th USENIX Security Symposium (USENIX Security\u201920). 2289\u20132306."},{"key":"e_1_3_3_110_2","doi-asserted-by":"publisher","DOI":"10.1145\/1297846.1297902"},{"key":"e_1_3_3_111_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.37"},{"key":"e_1_3_3_112_2","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3339002"},{"key":"e_1_3_3_113_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"e_1_3_3_114_2","first-page":"58","volume-title":"Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"Peters Dennis","year":"1994","unstructured":"Dennis Peters and David L. Parnas. 1994. Generating a test oracle from program documentation: Work in progress. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis. 58\u201365."},{"key":"e_1_3_3_115_2","first-page":"92","volume-title":"International Conference on Technical Formal Methods","author":"Poll Erik","year":"2009","unstructured":"Erik Poll. 2009. Teaching program specification and verification using JML and ESC\/Java2. In International Conference on Technical Formal Methods. Springer, 92\u2013104."},{"key":"e_1_3_3_116_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276517"},{"key":"e_1_3_3_117_2","article-title":"Not all bytes are equal: Neural byte sieve for fuzzing","author":"Rajpal Mohit","year":"2017","unstructured":"Mohit Rajpal, William Blum, and Rishabh Singh. 2017. Not all bytes are equal: Neural byte sieve for fuzzing. arXiv:1711.04596. Retrieved from https:\/\/arxiv.org\/abs\/1711.04596","journal-title":"arXiv:1711.04596"},{"key":"e_1_3_3_118_2","first-page":"49","volume-title":"Proceedings of the 24th USENIX Security Symposium (USENIX Security\u201915)","author":"Ramos David A.","year":"2015","unstructured":"David A. Ramos and Dawson Engler. 2015. Under-constrained symbolic execution: Correctness checking for real code. In Proceedings of the 24th USENIX Security Symposium (USENIX Security\u201915). 49\u201364."},{"key":"e_1_3_3_119_2","first-page":"1","volume-title":"Proceedings of the Network and Distributed System Security Symposium (NDSS\u201917)","volume":"17","author":"Rawat Sanjay","year":"2017","unstructured":"Sanjay Rawat, Vivek Jain, Ashish Kumar, Lucian Cojocar, Cristiano Giuffrida, and Herbert Bos. 2017. VUzzer: Application-aware evolutionary fuzzing. In Proceedings of the Network and Distributed System Security Symposium (NDSS\u201917), Vol. 17. 1\u201314."},{"key":"e_1_3_3_120_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.210304"},{"key":"e_1_3_3_121_2","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"key":"e_1_3_3_122_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00010"},{"key":"e_1_3_3_123_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23368"},{"key":"e_1_3_3_124_2","first-page":"373","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Visser Willem","year":"2020","unstructured":"Willem Visser and Jaco Geldenhuys. 2020. COASTAL: Combining concolic and fuzzing for Java (competition contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 373\u2013377."},{"key":"e_1_3_3_125_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007512.1007526"},{"key":"e_1_3_3_126_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183440.3183494"},{"key":"e_1_3_3_127_2","first-page":"497","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Wang Tielei","year":"2010","unstructured":"Tielei Wang, Tao Wei, Guofei Gu, and Wei Zou. 2010. TaintScope: A checksum-aware directed fuzzing tool for automatic software vulnerability detection. In Proceedings of the IEEE Symposium on Security and Privacy. IEEE, 497\u2013512."},{"key":"e_1_3_3_128_2","first-page":"603","volume-title":"Proceedings of the IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI\u201920)","author":"Wang Xiajing","year":"2020","unstructured":"Xiajing Wang, Changzhen Hu, Rui Ma, Binbin Li, and Xuefei Wang. 2020. LAFuzz: Neural network for efficient fuzzing. In Proceedings of the IEEE 32nd International Conference on Tools with Artificial Intelligence (ICTAI\u201920). IEEE, 603\u2013611."},{"key":"e_1_3_3_129_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_3_130_2","first-page":"70","volume-title":"International Workshop on Formal Approaches to Software Testing","author":"Xu Guoqing","year":"2003","unstructured":"Guoqing Xu and Zongyuang Yang. 2003. JMLAutoTest: A novel automated testing framework based on JML and JUnit. In International Workshop on Formal Approaches to Software Testing. Springer, 70\u201385."},{"key":"e_1_3_3_131_2","doi-asserted-by":"publisher","DOI":"10.1145\/1189256.1189259"},{"key":"e_1_3_3_132_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2936235"},{"key":"e_1_3_3_133_2","unstructured":"Michal Zalewski. 2014. Technical \u201cwhitepaper\u201d for afl-fuzz. Retrieved from http:\/\/lcamtuf.coredump.cx\/afl\/technical_details.txt"},{"key":"e_1_3_3_134_2","first-page":"489","volume-title":"Proceedings of the Conference on Internet Measurement Conference","author":"Zhang Liang","year":"2014","unstructured":"Liang Zhang, David Choffnes, Dave Levin, Tudor Dumitra\u015f, Alan Mislove, Aaron Schulman, and Christo Wilson. 2014. Analysis of SSL certificate reissues and revocations in the wake of heartbleed. In Proceedings of the Conference on Internet Measurement Conference. ACM, 489\u2013502."},{"key":"e_1_3_3_135_2","doi-asserted-by":"publisher","DOI":"10.1145\/3512345"},{"key":"e_1_3_3_136_2","first-page":"183","volume-title":"International Conference on Formal Verification of Object-Oriented Software","author":"Zimmerman Daniel M","year":"2010","unstructured":"Daniel M Zimmerman and Rinkesh Nagmoti. 2010. JMLUnit: The next generation. In International Conference on Formal Verification of Object-Oriented Software. Springer, 183\u2013197."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607538","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607538","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:28Z","timestamp":1750178188000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607538"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,20]]},"references-count":135,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3,31]]}},"alternative-id":["10.1145\/3607538"],"URL":"https:\/\/doi.org\/10.1145\/3607538","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,3,20]]},"assertion":[{"value":"2022-04-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}