{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:28:27Z","timestamp":1783740507582,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,4,12]],"date-time":"2026-04-12T00:00:00Z","timestamp":1775952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1755890, CCF-2139845, CCF-2124116"],"award-info":[{"award-number":["CCF-1755890, CCF-2139845, CCF-2124116"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,4,12]]},"DOI":"10.1145\/3793656.3793700","type":"proceedings-article","created":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T15:00:53Z","timestamp":1783695653000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Profile-Guided Constraint Simplification for Symbolic Execution"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-9103-0839","authenticated-orcid":false,"given":"Roxana","family":"Shajarian","sequence":"first","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, Nebraska, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3417-4352","authenticated-orcid":false,"given":"Md Rashedul","family":"Hasan","sequence":"additional","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3465-4056","authenticated-orcid":false,"given":"Lisong","family":"Xu","sequence":"additional","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6686-466X","authenticated-orcid":false,"given":"Hamid","family":"Bagheri","sequence":"additional","affiliation":[{"name":"School of Computing, University of Nebraska-Lincoln, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,7,10]]},"reference":[{"key":"e_1_3_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397347"},{"key":"e_1_3_3_1_3_2","doi-asserted-by":"crossref","unstructured":"Saswat Anand Edmund\u00a0K Burke Tsong\u00a0Yueh Chen John Clark Myra\u00a0B Cohen Wolfgang Grieskamp Mark Harman Mary\u00a0Jean Harrold and Phil Mcminn. 2013. An orchestrated survey of methodologies for automated software test case generation. Journal of Systems and Software 86 8 (2013) 1978\u20132001. doi:10.1016\/j.jss.2013.02.061","DOI":"10.1016\/j.jss.2013.02.061"},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2016.53"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Roberto Baldoni Emilio Coppa Daniele\u00a0Cono D\u2019elia Camil Demetrescu and Irene Finocchi. 2018. A survey of symbolic execution techniques. Comput. Surveys 51 3 1\u201339. doi:10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"e_1_3_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"crossref","unstructured":"Clark Barrett Roberto Sebastiani Sanjit\u00a0A Seshia and Cesare Tinelli. 2009. Satisfiability modulo theories. 185 (2009) 825\u2013885. doi:10.3233\/978-1-58603-929-5-825","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_3_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792770"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786842"},{"key":"e_1_3_3_1_11_2","first-page":"209","volume-title":"OSDI","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, Dawson\u00a0R Engler, et\u00a0al. 2008. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.. In OSDI , Vol.\u00a08. 209\u2013224."},{"key":"e_1_3_3_1_12_2","doi-asserted-by":"crossref","unstructured":"Cristian Cadar Patrice Godefroid Sarfraz Khurshid Corina\u00a0S Pasareanu Koushik Sen Nikolai Tillmann and Willem Visser. 2011. Symbolic execution for software testing in practice: preliminary assessment. (2011) 1066\u20131071. doi:10.1145\/1985793.1985995","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"crossref","unstructured":"Cristian Cadar and Koushik Sen. 2013. Symbolic execution for software testing: three decades later. Commun. ACM 56 2 (2013) 82\u201390. doi:10.1145\/2408776.2408795","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Michael\u00a0D Ernst Jeff\u00a0H Perkins Philip\u00a0J Guo Stephen McCamant Carlos Pacheco Matthew\u00a0S Tschantz and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69 1-3 (2007) 35\u201345. doi:10.1016\/j.scico.2007.01.015","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Nils Klarlund and Koushik Sen. 2005. DART: directed automated random testing. SIGPLAN Not. 40 6 (June 2005) 213\u2013223. doi:10.1145\/1064978.1065036","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_3_3_1_20_2","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Michael\u00a0Y Levin and David Molnar. 2012. SAGE: whitebox fuzzing for security testing. Commun. ACM 55 3 40\u201344. doi:10.1145\/2093548.2093564","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_3_1_21_2","series-title":"(ASE \u201922)","volume-title":"Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering","author":"Guti\u00e9rrez\u00a0Brida Sim\u00f3n","year":"2023","unstructured":"Sim\u00f3n Guti\u00e9rrez\u00a0Brida, Germ\u00e1n Regis, Guolong Zheng, Hamid Bagheri, Thanhvu Nguyen, Nazareno Aguirre, and Marcelo Frias. 2023. ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications. In Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (Rochester, MI, USA) (ASE \u201922). Association for Computing Machinery, New York, NY, USA, Article 55, 13\u00a0pages. doi:10.1145\/3551349.3556944"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31157-5_3"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"crossref","unstructured":"James\u00a0C King. 1976. Symbolic execution and program testing. Commun. ACM 19 7 (1976) 385\u2013394. doi:10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2015.7381839"},{"key":"e_1_3_3_1_28_2","first-page":"149","volume-title":"International Conference on Software Testing, Verification and Validation","author":"Palikareva Hristina","year":"2016","unstructured":"Hristina Palikareva, Tomasz Kuchta, and Cristian Cadar. 2016. Quantifying the complexity of constraint solving in symbolic execution. In International Conference on Software Testing, Verification and Validation. IEEE, 149\u2013160. doi:10.1109\/ICST.2016.24"},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_3_1_30_2","first-page":"804","volume-title":"IEEE Symposium on Security and Privacy (SP)","author":"Poeplau Sebastian","year":"2020","unstructured":"Sebastian Poeplau and Aur\u00e9lien Francillon. 2020. SymCC: efficient compiler-based symbolic execution. In IEEE Symposium on Security and Privacy (SP). IEEE, 804\u2013821."},{"key":"e_1_3_3_1_31_2","first-page":"49","volume-title":"24th USENIX Security Symposium","author":"Ramos David\u00a0A","year":"2015","unstructured":"David\u00a0A Ramos and Dawson\u00a0R Engler. 2015. Under-constrained symbolic execution: Correctness checking for real code. In 24th USENIX Security Symposium. USENIX Association, 49\u201364."},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321746"},{"key":"e_1_3_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_3_1_34_2","doi-asserted-by":"crossref","unstructured":"Roxana Shajarian Md\u00a0Rashedul Hasan Lisong Xu and Hamid Bagheri. 2026. Profile-Guided Constraint Simplification for Symbolic Execution: Artifact. doi:10.6084\/m9.figshare.30434338FormaliSE 2026 Artifact - Dataset.","DOI":"10.1145\/3793656.3793700"},{"key":"e_1_3_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23368"},{"key":"e_1_3_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP61940.2024.10858512"},{"key":"e_1_3_3_1_39_2","unstructured":"Qianqian Wang. 2019. Improving In-House Testing Using Field Execution Data. Ph.\u00a0D. Dissertation. Georgia Institute of Technology Atlanta GA USA. https:\/\/repository.gatech.edu\/server\/api\/core\/bitstreams\/fbbb8c33-f80f-4852-afda-249c1cb047a4\/content"},{"key":"e_1_3_3_1_40_2","series-title":"(SEC\u201918)","first-page":"745","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium","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 Proceedings of the 27th USENIX Conference on Security Symposium (Baltimore, MD, USA) (SEC\u201918). USENIX Association, USA, 745\u2013761."}],"event":{"name":"FormaliSE '26: IEEE\/ACM 14th International Conference on Formal Methods in Software Engineering","location":"Rio de Janeiro Brazil","acronym":"FormaliSE '26","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the IEEE\/ACM 14th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3793656.3793700","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T15:22:34Z","timestamp":1783696954000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3793656.3793700"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,12]]},"references-count":39,"alternative-id":["10.1145\/3793656.3793700","10.1145\/3793656"],"URL":"https:\/\/doi.org\/10.1145\/3793656.3793700","relation":{},"subject":[],"published":{"date-parts":[[2026,4,12]]},"assertion":[{"value":"2026-07-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}