{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:03:29Z","timestamp":1784232209350,"version":"3.55.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":["N6600 1-22-C-4027"],"award-info":[{"award-number":["N6600 1-22-C-4027"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-SHF 2321680"],"award-info":[{"award-number":["CCF-SHF 2321680"]}],"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":[[2025,1,7]]},"abstract":"<jats:p>\n                    We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed in\n                    <jats:italic toggle=\"yes\">Linear Temporal Logic over Finite Traces<\/jats:italic>\n                    (LTL\n                    <jats:sub>f<\/jats:sub>\n                    ), interpreting them as\n                    <jats:italic toggle=\"yes\">symbolic finite automata<\/jats:italic>\n                    (SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion of\n                    <jats:italic toggle=\"yes\">symbolic derivatives<\/jats:italic>\n                    , a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach.\n                  <\/jats:p>","DOI":"10.1145\/3704886","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1475-1505","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Derivative-Guided Symbolic Execution"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2619-2288","authenticated-orcid":false,"given":"Yongwei","family":"Yuan","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-7501","authenticated-orcid":false,"given":"Zhe","family":"Zhou","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7490-8500","authenticated-orcid":false,"given":"Julia","family":"Belyakova","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6871-2424","authenticated-orcid":false,"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_96"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297070"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45329-8_11"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90088-5"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21254-3_13"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297069"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535849"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2540128.2540252"},{"key":"e_1_3_2_16_1","first-page":"1558","volume-title":"Proceedings of the 24th International Conference on Artificial Intelligence (IJCAI\u201915)","author":"Giacomo Giuseppe De","year":"2015","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2015. Synthesis for LTL and LDL on Finite Traces. In Proceedings of the 24th International Conference on Artificial Intelligence (IJCAI\u201915). AAAI Press, Buenos Aires, Argentina, 1558\u20131564."},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103845.1094841"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314618"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00253-1"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2014.175"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.25"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034801"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000096"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628156"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158139"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/580840"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018436"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_8"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_5"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384655"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2010.15"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480889"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13800040"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Yongwei Yuan Zhe Zhou Julia Belyakova and Suresh Jagannathan. 2024b. Derivative-Guided Symbolic Execution. https:\/\/doi.org\/10.48550\/arXiv.2411.02716 10.48550\/arXiv.2411.02716 2411.02716","DOI":"10.48550\/arXiv.2411.02716"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.80"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704886","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:27Z","timestamp":1770200067000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704886"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704886"],"URL":"https:\/\/doi.org\/10.1145\/3704886","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}