{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T13:02:31Z","timestamp":1785243751612,"version":"3.55.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-16-C-0022,HR0011-18-C-0011"],"award-info":[{"award-number":["FA8750-16-C-0022,HR0011-18-C-0011"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1421243,1521523"],"award-info":[{"award-number":["1421243,1521523"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Property-based random testing, exemplified by frameworks such as Haskell's QuickCheck, works by testing an executable predicate (a property) on a stream of randomly generated inputs. Property testing works very well in many cases, but not always. Some properties are conditioned on the input satisfying demanding semantic invariants that are not consequences of its syntactic structure---e.g., that an input list must be sorted or have no duplicates. Most randomly generated inputs fail to satisfy properties with such sparse preconditions, and so are simply discarded. As a result, much of the target system may go untested.<\/jats:p>\n          <jats:p>We address this issue with a novel technique called coverage guided, property based testing (CGPT). Our approach is inspired by the related area of coverage guided fuzzing, exemplified by tools like AFL. Rather than just generating a fresh random input at each iteration, CGPT can also produce new inputs by mutating previous ones using type-aware, generic mutator operators. The target program is instrumented to track which control flow branches are executed during a run and inputs whose runs expand control-flow coverage are retained for future mutations. This means that, when sparse conditions in the target are satisfied and new coverage is observed, the input that triggered them will be retained and used as a springboard to go further.<\/jats:p>\n          <jats:p>We have implemented CGPT as an extension to the QuickChick property testing tool for Coq programs; we call our implementation FuzzChick. We evaluate FuzzChick on two Coq developments for abstract machines that aim to enforce flavors of noninterference, which has a (very) sparse precondition. We systematically inject bugs in the machines' checking rules and use FuzzChick to look for counterexamples to the claim that they satisfy a standard noninterference property. We find that vanilla QuickChick almost always fails to find any bugs after a long period of time, as does an earlier proposal for combining property testing and fuzzing. In contrast, FuzzChick often finds them within seconds to minutes. Moreover, FuzzChick is almost fully automatic; although highly tuned, hand-written generators can find the bugs faster, they require substantial amounts of insight and manual effort.<\/jats:p>","DOI":"10.1145\/3360607","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["Coverage guided, property based testing"],"prefix":"10.1145","volume":"3","author":[{"given":"Leonidas","family":"Lampropoulos","sequence":"first","affiliation":[{"name":"University of Maryland, USA \/ University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"AFL 2018. American Fuzzing Lop (AFL). http:\/\/lcamtuf.coredump.cx\/afl\/ .  AFL 2018. American Fuzzing Lop (AFL). http:\/\/lcamtuf.coredump.cx\/afl\/ ."},{"key":"e_1_2_2_2_1","volume-title":"Workshop on Programming Languages and Analysis for Security (PLAS) (PLAS). ACM, 113\u2013124","author":"Thomas","unstructured":"Thomas H. Austin and Cormac Flanagan. 2009. Efficient purely-dynamic information flow analysis . In Workshop on Programming Languages and Analysis for Security (PLAS) (PLAS). ACM, 113\u2013124 . http:\/\/slang.soe.ucsc.edu\/cormac\/ papers\/plas09.pdf Thomas H. Austin and Cormac Flanagan. 2009. Efficient purely-dynamic information flow analysis. In Workshop on Programming Languages and Analysis for Security (PLAS) (PLAS). ACM, 113\u2013124. http:\/\/slang.soe.ucsc.edu\/cormac\/ papers\/plas09.pdf"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535839"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Osbert Bastani Rahul Sharma Alex Aiken and Percy Liang. 2017. Synthesizing Program Input Grammars. In PLDI.  Osbert Bastani Rahul Sharma Alex Aiken and Percy Liang. 2017. Synthesizing Program Input Grammars. In PLDI.","DOI":"10.1145\/3062341.3062349"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"e_1_2_2_7_1","volume-title":"Coverage-based Greybox Fuzzing As Markov Chain. In ACM SIGSAC Conference on Computer and Communications Security (CCS).","author":"B\u00f6hme Marcel","year":"2016","unstructured":"Marcel B\u00f6hme , Van-Thuan Pham , and Abhik Roychoudhury . 2016 . Coverage-based Greybox Fuzzing As Markov Chain. In ACM SIGSAC Conference on Computer and Communications Security (CCS). Marcel B\u00f6hme, Van-Thuan Pham, and Abhik Roychoudhury. 2016. Coverage-based Greybox Fuzzing As Markov Chain. In ACM SIGSAC Conference on Computer and Communications Security (CCS)."},{"key":"e_1_2_2_8_1","volume-title":"2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science)","volume":"7679","author":"Bulwahn Lukas","year":"2012","unstructured":"Lukas Bulwahn . 2012 a. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof . In 2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science) , Vol. 7679 . Springer, 92\u2013108. https:\/\/www.irisa.fr\/celtique\/genet\/ACF\/BiblioIsabelle\/quickcheckNew.pdf Lukas Bulwahn. 2012a. The New Quickcheck for Isabelle - Random, Exhaustive and Symbolic Testing under One Roof. In 2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science), Vol. 7679. Springer, 92\u2013108. https:\/\/www.irisa.fr\/celtique\/genet\/ACF\/BiblioIsabelle\/quickcheckNew.pdf"},{"key":"e_1_2_2_9_1","volume-title":"Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science)","volume":"7180","author":"Bulwahn Lukas","year":"2012","unstructured":"Lukas Bulwahn . 2012 b. Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science) , Vol. 7180 . Springer, 153\u2013167. Lukas Bulwahn. 2012b. Smart Testing of Functional Programs in Isabelle. In 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science), Vol. 7180. Springer, 153\u2013167."},{"key":"e_1_2_2_10_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI.","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00046"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/THS.2013.6699066"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503784"},{"key":"e_1_2_2_16_1","volume-title":"DIF UZE: Interface Aware Fuzzing for Kernel Drivers. In ACM SIGSAC Conference on Computer and Communications Security (CCS).","author":"Corina Jake","year":"2017","unstructured":"Jake Corina , Aravind Machiry , Christopher Salls , Yan Shoshitaishvili , Shuang Hao , Christopher Kruegel , and Giovanni Vigna . 2017 . DIF UZE: Interface Aware Fuzzing for Kernel Drivers. In ACM SIGSAC Conference on Computer and Communications Security (CCS). Jake Corina, Aravind Machiry, Christopher Salls, Yan Shoshitaishvili, Shuang Hao, Christopher Kruegel, and Giovanni Vigna. 2017. DIF UZE: Interface Aware Fuzzing for Kernel Drivers. In ACM SIGSAC Conference on Computer and Communications Security (CCS)."},{"key":"e_1_2_2_17_1","unstructured":"Crowbar 2017. Crowbar. https:\/\/github.com\/stedolan\/crowbar .  Crowbar 2017. Crowbar. https:\/\/github.com\/stedolan\/crowbar ."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.210.3"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_20_1","volume-title":"The Coq Workshop. http:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/talks\/coq6_ submission_4.pdf","author":"D\u00e9n\u00e8s Maxime","unstructured":"Maxime D\u00e9n\u00e8s , C\u0103t\u0103lin Hri\u0163cu , Leonidas Lampropoulos , Zoe Paraskevopoulou , and Benjamin C. Pierce . 2014. QuickChick: Property-based testing for Coq . The Coq Workshop. http:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/talks\/coq6_ submission_4.pdf Maxime D\u00e9n\u00e8s, C\u0103t\u0103lin Hri\u0163cu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. 2014. QuickChick: Property-based testing for Coq. The Coq Workshop. http:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/talks\/coq6_ submission_4.pdf"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_2_2_22_1","unstructured":"Shuitao Gan Chao Zhang Xiaojun Qin Xuwen Tu Kang Li Zhongyu Pei and Zuoning Chen. 2018. CollAFL: Path Sensitive Fuzzing. In S&amp;P.  Shuitao Gan Chao Zhang Xiaojun Qin Xuwen Tu Kang Li Zhongyu Pei and Zuoning Chen. 2018. CollAFL: Path Sensitive Fuzzing. In S&amp;P."},{"key":"e_1_2_2_23_1","volume-title":"Hails: Protecting Data Privacy in Untrusted Web Applications. In 10th Symposium on Operating Systems Design and Implementation (OSDI). USENIX, 47\u201360","author":"Giffin Daniel B.","year":"2012","unstructured":"Daniel B. Giffin , Amit Levy , Deian Stefan , David Terei , David Mazi\u00e8res , John Mitchell , and Alejandro Russo . 2012 . Hails: Protecting Data Privacy in Untrusted Web Applications. In 10th Symposium on Operating Systems Design and Implementation (OSDI). USENIX, 47\u201360 . http:\/\/www.scs.stanford.edu\/~deian\/pubs\/\/giffin:2012:hails.pdf Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazi\u00e8res, John Mitchell, and Alejandro Russo. 2012. Hails: Protecting Data Privacy in Untrusted Web Applications. In 10th Symposium on Operating Systems Design and Implementation (OSDI). USENIX, 47\u201360. http:\/\/www.scs.stanford.edu\/~deian\/pubs\/\/giffin:2012:hails.pdf"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_2_2_25_1","volume-title":"Levin","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Adam Kiezun , and Michael Y . Levin . 2008 a. Grammar-based Whitebox Fuzzing. In PLDI. Patrice Godefroid, Adam Kiezun, and Michael Y. Levin. 2008a. Grammar-based Whitebox Fuzzing. In PLDI."},{"key":"e_1_2_2_26_1","volume-title":"Molnar","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Michael Y. Levin , and David A . Molnar . 2008 b. Automated Whitebox Fuzz Testing. In NDSS. Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008b. Automated Whitebox Fuzz Testing. In NDSS."},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Hila Peleg and Rishabh Singh. 2017. Learn&amp;#38;Fuzz: Machine Learning for Input Fuzzing. In ASE.  Patrice Godefroid Hila Peleg and Rishabh Singh. 2017. Learn&amp;#38;Fuzz: Machine Learning for Input Fuzzing. In ASE.","DOI":"10.1109\/ASE.2017.8115618"},{"key":"e_1_2_2_28_1","volume-title":"Goguen and Jos\u00c3\u013e Meseguer","author":"Joseph","year":"1982","unstructured":"Joseph A. Goguen and Jos\u00c3\u013e Meseguer . 1982 . Security Policies and Security Models. In S &amp;P. Joseph A. Goguen and Jos\u00c3\u013e Meseguer. 1982. Security Policies and Security Models. In S&amp;P."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976017"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Gustavo Grieco Martn Ceresa Agustn Mista and Pablo Buiras. 2017. QuickFuzz Testing for Fun and Profit. J. Syst. Softw. (2017).  Gustavo Grieco Martn Ceresa Agustn Mista and Pablo Buiras. 2017. QuickFuzz Testing for Fun and Profit. J. Syst. Softw. (2017).","DOI":"10.1016\/j.jss.2017.09.018"},{"key":"e_1_2_2_31_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA , November 2-4, 2016. 653\u2013669. https: \/\/www.usenix.org\/conference\/osdi16\/technical- sessions\/presentation\/gu Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016. 653\u2013669. https: \/\/www.usenix.org\/conference\/osdi16\/technical- sessions\/presentation\/gu"},{"key":"e_1_2_2_32_1","volume-title":"All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 3\u201317","author":"Hri\u0163cu C\u0103t\u0103lin","year":"2013","unstructured":"C\u0103t\u0103lin Hri\u0163cu , Michael Greenberg , Ben Karel , Benjamin C. Pierce , and Greg Morrisett . 2013 a. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 3\u201317 . http:\/\/www.crashsafe.org\/node\/23 C\u0103t\u0103lin Hri\u0163cu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. 2013a. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy. IEEE Computer Society Press, 3\u201317. http:\/\/www.crashsafe.org\/node\/23"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500574"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000058"},{"key":"e_1_2_2_35_1","volume-title":"Software Abstractions: Logic, Language, and Anlysis","author":"Jackson Daniel","year":"2011","unstructured":"Daniel Jackson . 2011 . Software Abstractions: Logic, Language, and Anlysis . The MIT Press . http:\/\/alloy.mit.edu\/alloy\/book.html Daniel Jackson. 2011. Software Abstractions: Logic, Language, and Anlysis. The MIT Press. http:\/\/alloy.mit.edu\/alloy\/book.html"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274746"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243804"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_2_2_41_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018","unstructured":"Leonidas Lampropoulos and Benjamin C . Pierce . 2018 . QuickCHick: Property- Based Testing In Coq. Electronic textbook. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf Leonidas Lampropoulos and Benjamin C. Pierce. 2018. QuickCHick: Property-Based Testing In Coq. Electronic textbook. http:\/\/www.cis.upenn.edu\/~bcpierce\/sf"},{"key":"e_1_2_2_42_1","volume-title":"FairFuzz: A Targeted Mutation Strategy for Increasing Greybox Fuzz Testing Coverage. IEEE\/ACM International Conference on Automated Software Engineering.","author":"Lemieux Caroline","year":"2018","unstructured":"Caroline Lemieux and Koushik Sen . 2018 . FairFuzz: A Targeted Mutation Strategy for Increasing Greybox Fuzz Testing Coverage. IEEE\/ACM International Conference on Automated Software Engineering. Caroline Lemieux and Koushik Sen. 2018. FairFuzz: A Targeted Mutation Strategy for Increasing Greybox Fuzz Testing Coverage. IEEE\/ACM International Conference on Automated Software Engineering."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/96267.96279"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2013.8"},{"key":"e_1_2_2_46_1","volume-title":"Zest: Validity Fuzzing and Parametric Generators for Effective Random Testing. CoRR abs\/1812.00078","author":"Padhye Rohan","year":"2018","unstructured":"Rohan Padhye , Caroline Lemieux , Koushik Sen , Mike Papadakis , and Yves Le Traon . 2018 . Zest: Validity Fuzzing and Parametric Generators for Effective Random Testing. CoRR abs\/1812.00078 (2018). Rohan Padhye, Caroline Lemieux, Koushik Sen, Mike Papadakis, and Yves Le Traon. 2018. Zest: Validity Fuzzing and Parametric Generators for Effective Random Testing. CoRR abs\/1812.00078 (2018)."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034663"},{"key":"e_1_2_2_48_1","volume-title":"Workshop on Coq for PL. https:\/\/coqpl.cs.washington.edu\/wpcontent\/uploads\/2014\/12\/quickchick.pdf","author":"Paraskevopoulou Zoe","unstructured":"Zoe Paraskevopoulou , C\u0103t\u0103lin Hri\u0163cu , Maxime D\u00e9n\u00e8s , Leonidas Lampropoulos , and Benjamin C. Pierce . 2015a. A Coq Framework For Verified Property-Based Testing . Workshop on Coq for PL. https:\/\/coqpl.cs.washington.edu\/wpcontent\/uploads\/2014\/12\/quickchick.pdf Zoe Paraskevopoulou, C\u0103t\u0103lin Hri\u0163cu, Maxime D\u00e9n\u00e8s, Leonidas Lampropoulos, and Benjamin C. Pierce. 2015a. A Coq Framework For Verified Property-Based Testing. Workshop on Coq for PL. https:\/\/coqpl.cs.washington.edu\/wpcontent\/uploads\/2014\/12\/quickchick.pdf"},{"key":"e_1_2_2_49_1","volume-title":"Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.)","volume":"9236","author":"Paraskevopoulou Zoe","unstructured":"Zoe Paraskevopoulou , C\u0103t\u0103lin Hri\u0163cu , Maxime D\u00e9n\u00e8s , Leonidas Lampropoulos , and Benjamin C. Pierce . 2015b . Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.) , Vol. 9236 . Springer, 325\u2013343. http:\/\/prosecco.gforge.inria.fr\/ personal\/hritcu\/publications\/foundational- pbt.pdf Zoe Paraskevopoulou, C\u0103t\u0103lin Hri\u0163cu, Maxime D\u00e9n\u00e8s, Leonidas Lampropoulos, and Benjamin C. Pierce. 2015b. Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.), Vol. 9236. Springer, 325\u2013343. http:\/\/prosecco.gforge.inria.fr\/ personal\/hritcu\/publications\/foundational- pbt.pdf"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00056"},{"key":"e_1_2_2_51_1","volume-title":"Alexandru Razvan Caciulescu, and Abhik Roychoudhury","author":"Pham Van-Thuan","year":"2018","unstructured":"Van-Thuan Pham , Marcel B\u00f6hme , Andrew E. Santosa , Alexandru Razvan Caciulescu, and Abhik Roychoudhury . 2018 . Smart Greybox Fuzzing. CoRR abs\/1811.09447 (2018). arXiv: 1811.09447 http:\/\/arxiv.org\/abs\/1811.09447 Van-Thuan Pham, Marcel B\u00f6hme, Andrew E. Santosa, Alexandru Razvan Caciulescu, and Abhik Roychoudhury. 2018. Smart Greybox Fuzzing. CoRR abs\/1811.09447 (2018). arXiv: 1811.09447 http:\/\/arxiv.org\/abs\/1811.09447"},{"key":"e_1_2_2_52_1","volume-title":"Vuzzer: Applicationaware evolutionary fuzzing. In NDSS.","author":"Rawat Sanjay","year":"2017","unstructured":"Sanjay Rawat , Vivek Jain , Ashish Kumar , Lucian Cojocar , Cristiano Giuffrida , and Herbert Bos . 2017 . Vuzzer: Applicationaware evolutionary fuzzing. In NDSS. Sanjay Rawat, Vivek Jain, Ashish Kumar, Lucian Cojocar, Cristiano Giuffrida, and Herbert Bos. 2017. Vuzzer: Applicationaware evolutionary fuzzing. In NDSS."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_2_55_1","doi-asserted-by":"crossref","unstructured":"Bhargava Shastry Markus Leutner Tobias Fiebig Kashyap Thimmaraju Fabian Yamaguchi Konrad Rieck Stefan Schmid Jean-Pierre Seifert and Anja Feldmann. 2017. Static Program Analysis as a Fuzzing Aid. In Research in Attacks Intrusions and Defenses (RAID).  Bhargava Shastry Markus Leutner Tobias Fiebig Kashyap Thimmaraju Fabian Yamaguchi Konrad Rieck Stefan Schmid Jean-Pierre Seifert and Anja Feldmann. 2017. Static Program Analysis as a Fuzzing Aid. In Research in Attacks Intrusions and Defenses (RAID).","DOI":"10.1007\/978-3-319-66332-6_2"},{"key":"e_1_2_2_56_1","volume-title":"Mitchell","author":"Stefan Deian","year":"2012","unstructured":"Deian Stefan , Alejandro Russo , David Mazi\u00e8res , and John C . Mitchell . 2012 . Disjunction Category Labels. In NordSec . Deian Stefan, Alejandro Russo, David Mazi\u00e8res, and John C. Mitchell. 2012. Disjunction Category Labels. In NordSec."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034688"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23368"},{"key":"e_1_2_2_59_1","volume-title":"Kodkod: A Relational Model Finder. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science)","volume":"4424","author":"Torlak Emina","year":"2007","unstructured":"Emina Torlak and Daniel Jackson . 2007 . Kodkod: A Relational Model Finder. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science) , Vol. 4424 . Springer, 632\u2013647. http:\/\/people.csail.mit.edu\/emina\/pubs\/kodkod.tacas07.pdf Emina Torlak and Daniel Jackson. 2007. Kodkod: A Relational Model Finder. In 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), Vol. 4424. Springer, 632\u2013647. http:\/\/people.csail.mit.edu\/emina\/pubs\/kodkod.tacas07.pdf"},{"key":"e_1_2_2_60_1","volume-title":"Skyfire: Data-Driven Seed Generation for Fuzzing. In IEEE Symposium on Security and Privacy (S&amp;P).","author":"Wang Junjie","year":"2017","unstructured":"Junjie Wang , Bihuan Chen , Lei Wei , and Yang Liu . 2017 . Skyfire: Data-Driven Seed Generation for Fuzzing. In IEEE Symposium on Security and Privacy (S&amp;P). Junjie Wang, Bihuan Chen, Lei Wei, and Yang Liu. 2017. Skyfire: Data-Driven Seed Generation for Fuzzing. In IEEE Symposium on Security and Privacy (S&amp;P)."},{"key":"e_1_2_2_61_1","volume-title":"Superion: Grammar-Aware Greybox Fuzzing. CoRR abs\/1812.01197","author":"Wang Junjie","year":"2018","unstructured":"Junjie Wang , Bihuan Chen , Lei Wei , and Yang Liu . 2018 . Superion: Grammar-Aware Greybox Fuzzing. CoRR abs\/1812.01197 (2018). Junjie Wang, Bihuan Chen, Lei Wei, and Yang Liu. 2018. Superion: Grammar-Aware Greybox Fuzzing. CoRR abs\/1812.01197 (2018)."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.10.027"},{"key":"e_1_2_2_63_1","volume-title":"27th USENIX Security Symposium (USENIX Security 18)","author":"Yun Insu","year":"2018","unstructured":"Insu Yun , Sangho Lee , Meng Xu , Yeongjin Jang , and Taesoo Kim . 2018 . QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing . In 27th USENIX Security Symposium (USENIX Security 18) . USENIX Association, Baltimore, MD, 745\u2013761. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/yun Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2018. QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing. In 27th USENIX Security Symposium (USENIX Security 18). USENIX Association, Baltimore, MD, 745\u2013761. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/yun"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360607","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360607","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360607","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360607"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":61,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360607"],"URL":"https:\/\/doi.org\/10.1145\/3360607","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}