{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T17:22:27Z","timestamp":1792171347178,"version":"4.4.0"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T00:00:00Z","timestamp":1629244800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,8,20]]},"DOI":"10.1145\/3468264.3468540","type":"proceedings-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T01:44:18Z","timestamp":1629337458000},"page":"1141-1153","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Skeletal approximation enumeration for SMT solver testing"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-9518","authenticated-orcid":false,"given":"Peisen","family":"Yao","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heqing","family":"Huang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wensheng","family":"Tang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Qingkai","family":"Shi","sequence":"additional","affiliation":[{"name":"Ant Group, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rongxin","family":"Wu","sequence":"additional","affiliation":[{"name":"Xiamen University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Charles","family":"Zhang","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2014. AFL: american fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl\/ Accessed: 2014.  2014. AFL: american fuzzy lop. http:\/\/lcamtuf.coredump.cx\/afl\/ Accessed: 2014."},{"key":"e_1_3_2_1_2_1","unstructured":"2021. ddSMT.. https:\/\/github.com\/aniemetz\/ddSMT  2021. ddSMT.. https:\/\/github.com\/aniemetz\/ddSMT"},{"key":"e_1_3_2_1_3_1","unstructured":"2021. pyDelta.. https:\/\/github.com\/nafur\/pydelta  2021. pyDelta.. https:\/\/github.com\/nafur\/pydelta"},{"key":"e_1_3_2_1_4_1","unstructured":"2021. SMT-COMP.. https:\/\/smt-comp.github.io\/  2021. SMT-COMP.. https:\/\/smt-comp.github.io\/"},{"key":"e_1_3_2_1_5_1","unstructured":"2021. Z3 test scripts.. https:\/\/github.com\/Z3Prover\/z3\/src\/test  2021. Z3 test scripts.. https:\/\/github.com\/Z3Prover\/z3\/src\/test"},{"key":"e_1_3_2_1_6_1","unstructured":"2021. CVC4 regression test suit.. https:\/\/github.com\/CVC4\/CVC4\/test\/  2021. CVC4 regression test suit.. https:\/\/github.com\/CVC4\/CVC4\/test\/"},{"key":"e_1_3_2_1_7_1","unstructured":"2021. Yices2 regression test suit.. https:\/\/github.com\/SRI-CSL\/yices2\/tests  2021. Yices2 regression test suit.. https:\/\/github.com\/SRI-CSL\/yices2\/tests"},{"key":"e_1_3_2_1_8_1","unstructured":"2021. OpenSMT regression test suit.. https:\/\/github.com\/usi-verification-and-security\/opensmt\/regression  2021. OpenSMT regression test suit.. https:\/\/github.com\/usi-verification-and-security\/opensmt\/regression"},{"key":"e_1_3_2_1_9_1","unstructured":"2021. https:\/\/smtfuzz.github.io\/  2021. https:\/\/smtfuzz.github.io\/"},{"key":"e_1_3_2_1_10_1","volume-title":"NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019","author":"Aschermann Cornelius","year":"2019","unstructured":"Cornelius Aschermann , Tommaso Frassetto , Thorsten Holz , Patrick Jauernig , Ahmad-Reza Sadeghi , and Daniel Teuchert . 2019 . NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019 , San Diego, California, USA , February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/nautilus-fishing-for-deep-bugs-with-grammars\/ Cornelius Aschermann, Tommaso Frassetto, Thorsten Holz, Patrick Jauernig, Ahmad-Reza Sadeghi, and Daniel Teuchert. 2019. NAUTILUS: Fishing for Deep Bugs with Grammars. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019, San Diego, California, USA, February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/nautilus-fishing-for-deep-bugs-with-grammars\/"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_12_1","volume-title":"The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org, 15","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett , Aaron Stump , and Cesare Tinelli . 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org, 15 ( 2010 ), 18\u201352. Clark Barrett, Aaron Stump, and Cesare Tinelli. 2010. The satisfiability modulo theories library (SMT-LIB). www. SMT-LIB. org, 15 (2010), 18\u201352."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2017.1"},{"key":"e_1_3_2_1_14_1","volume-title":"Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017","author":"Blazytko Tim","year":"2017","unstructured":"Tim Blazytko , Moritz Contag , Cornelius Aschermann , and Thorsten Holz . 2017 . Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017 , Vancouver, BC, Canada , August 16-18, 2017, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 643\u2013659. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/blazytko Tim Blazytko, Moritz Contag, Cornelius Aschermann, and Thorsten Holz. 2017. Syntia: Synthesizing the Semantics of Obfuscated Code. In 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, Canada, August 16-18, 2017, Engin Kirda and Thomas Ristenpart (Eds.). USENIX Association, 643\u2013659. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/blazytko"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340923"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04772-5_40"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670413"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_28"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380398"},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908) . USENIX Association, Berkeley, CA, USA. 209\u2013224. http:\/\/dl.acm.org\/citation.cfm?id= 1855741.1855756 Cristian Cadar, Daniel Dunbar, and Dawson R Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, Berkeley, CA, USA. 209\u2013224. http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2005.67"},{"key":"e_1_3_2_1_25_1","unstructured":"Tsong Y Chen Shing C Cheung and Shiu Ming Yiu. 2020. Metamorphic testing: a new approach for generating next test cases. arXiv preprint arXiv:2002.12543.  Tsong Y Chen Shing C Cheung and Shiu Ming Yiu. 2020. Metamorphic testing: a new approach for generating next test cases. arXiv preprint arXiv:2002.12543."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1186\/1471-2105-10-24"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213858"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770421"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23263"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00063"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/64"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409763"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330576"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_2"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2941681"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428279"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_5"},{"key":"e_1_3_2_1_49_1","volume-title":"AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany , Derek Bruening , Alexander Potapenko , and Dmitriy Vyukov . 2012 . AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference , Boston, MA, USA , June 13-15, 2012, Gernot Heiser and Wilson C. Hsieh (Eds.). USENIX Association, 309\u2013318. https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/serebryany Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitriy Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In 2012 USENIX Annual Technical Conference, Boston, MA, USA, June 13-15, 2012, Gernot Heiser and Wilson C. Hsieh (Eds.). USENIX Association, 309\u2013318. https:\/\/www.usenix.org\/conference\/atc12\/technical-sessions\/presentation\/serebryany"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama and Rastislav Bodik. 2008. Program synthesis by sketching. Citeseer.  Armando Solar-Lezama and Rastislav Bodik. 2008. Program synthesis by sketching. Citeseer.","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984038"},{"key":"e_1_3_2_1_52_1","volume-title":"Gcov-using the gnu compiler collection (gcc). Online, dispon\u0131vel em http:\/\/gcc. gnu. org\/onlinedocs\/gcc\/Gcov. html-Ultimo acesso em, 26, 02","author":"Team G","year":"2014","unstructured":"G Team . 2014. Gcov-using the gnu compiler collection (gcc). Online, dispon\u0131vel em http:\/\/gcc. gnu. org\/onlinedocs\/gcc\/Gcov. html-Ultimo acesso em, 26, 02 ( 2014 ), 2015. G Team. 2014. Gcov-using the gnu compiler collection (gcc). Online, dispon\u0131vel em http:\/\/gcc. gnu. org\/onlinedocs\/gcc\/Gcov. html-Ultimo acesso em, 26, 02 (2014), 2015."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330567"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416563"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00081"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/25.4.465"},{"key":"e_1_3_2_1_58_1","first-page":"8","volume-title":"AerospaceLab","author":"Robert Delmas Virginie WIELS","year":"2012","unstructured":"Virginie WIELS , Robert Delmas , David Doose , Pierre-Lo\u00efc Garoche , J. Cazin , and Guy Durrieu . 2012 . Formal Verification of Critical Aerospace Software . AerospaceLab , May , p. 1\u2013 8 . https:\/\/hal.archives-ouvertes.fr\/hal-01184099 Virginie WIELS, Robert Delmas, David Doose, Pierre-Lo\u00efc Garoche, J. Cazin, and Guy Durrieu. 2012. Formal Verification of Critical Aerospace Software. AerospaceLab, May, p. 1\u20138. https:\/\/hal.archives-ouvertes.fr\/hal-01184099"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3464803"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2017.2772854"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48166-4_16"}],"event":{"name":"ESEC\/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Athens Greece","acronym":"ESEC\/FSE '21","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3468264.3468540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:50Z","timestamp":1750195490000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3468264.3468540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,18]]},"references-count":63,"alternative-id":["10.1145\/3468264.3468540","10.1145\/3468264"],"URL":"https:\/\/doi.org\/10.1145\/3468264.3468540","relation":{},"subject":[],"published":{"date-parts":[[2021,8,18]]},"assertion":[{"value":"2021-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}