{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,28]],"date-time":"2026-05-28T00:35:23Z","timestamp":1779928523104,"version":"3.53.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,10,7]],"date-time":"2014-10-07T00:00:00Z","timestamp":1412640000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000145","name":"Division of Information and Intelligent Systems","doi-asserted-by":"publisher","award":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"],"award-info":[{"award-number":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"]}],"id":[{"id":"10.13039\/100000145","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"],"award-info":[{"award-number":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-09-1-0351"],"award-info":[{"award-number":["FA9550-09-1-0351"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"],"award-info":[{"award-number":["IIS-0438967, CCF-0845628, CCF-1319688, and CNS-0958231"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,10,14]]},"abstract":"<jats:p>\n            The last few years have seen a resurgence of interest in the use of symbolic execution\u2014a program analysis technique developed more than three decades ago to analyze program execution paths. Scaling symbolic execution to real systems remains challenging despite recent algorithmic and technological advances. An effective approach to address scalability is to\n            <jats:italic>reduce<\/jats:italic>\n            the scope of the analysis. For example, in regression analysis,\n            <jats:italic>differences<\/jats:italic>\n            between two related program versions are used to guide the analysis. While such an approach is intuitive, finding efficient and precise ways to identify program differences, and characterize their impact on how the program executes has proved challenging in practice.\n          <\/jats:p>\n          <jats:p>\n            In this article, we present\n            <jats:italic>Directed Incremental Symbolic Execution<\/jats:italic>\n            (DiSE), a novel technique for detecting and characterizing the impact of program changes to scale symbolic execution. The novelty of DiSE is to combine the\n            <jats:italic>efficiencies<\/jats:italic>\n            of static analysis techniques to compute program difference information with the\n            <jats:italic>precision<\/jats:italic>\n            of symbolic execution to explore program execution paths and generate path conditions affected by the differences. DiSE complements other reduction and bounding techniques for improving symbolic execution. Furthermore, DiSE does not require analysis results to be carried forward as the software evolves\u2014only the source code for two related program versions is required. An experimental evaluation using our implementation of DiSE illustrates its effectiveness at detecting and characterizing the effects of program changes.\n          <\/jats:p>","DOI":"10.1145\/2629536","type":"journal-article","created":{"date-parts":[[2014,10,14]],"date-time":"2014-10-14T12:29:11Z","timestamp":1413289751000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["Directed Incremental Symbolic Execution"],"prefix":"10.1145","volume":"24","author":[{"given":"Guowei","family":"Yang","sequence":"first","affiliation":[{"name":"Texas State University, San Marcos, TX"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[{"name":"NASA Langley Research Center, Hampton, VA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, CA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sarfraz","family":"Khurshid","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, Austin, TX"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,10,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0090-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_3_1","volume-title":"Model Checking Software","author":"Backes John","unstructured":"John Backes , Suzette Person , Neha Rungta , and Oksana Tkachuk . 2013b. Regression verification using impact summaries . In Model Checking Software , Springer , 99--116. John Backes, Suzette Person, Neha Rungta, and Oksana Tkachuk. 2013b. Regression verification using impact summaries. In Model Checking Software, Springer, 99--116."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_5_1","volume-title":"Engler","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 OSDI. 209--224. 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 OSDI. 209--224."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1308173.1308253"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041564"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/367008.367020"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.40"},{"key":"e_1_2_1_18_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . The MIT Press , Cambridge, MA . Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge, MA."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11563228_10"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_12"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108817"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041563"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.v15:2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382801"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001425"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993558"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025152"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859083"},{"key":"e_1_2_1_34_1","volume-title":"Engler","author":"Ramos David A.","year":"2011","unstructured":"David A. Ramos and Dawson R . Engler . 2011 . Practical, low-effort equivalence verification of real code. In Proceedings of CAV. 669--685. David A. Ramos and Dawson R. Engler. 2011. Practical, low-effort equivalence verification of real code. In Proceedings of CAV. 669--685."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2012.6405261"},{"key":"e_1_2_1_36_1","unstructured":"SAE-ARP4761. 1996. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE International.  SAE-ARP4761. 1996. Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE International."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831733"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTE.2010.5608866"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384654"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986337"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571175"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001422"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC.2009.29"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of ICSM. 115--124","author":"Yang Guowei","year":"2009","unstructured":"Guowei Yang , Matthew B. Dwyer , and Gregg Rothermel . 2009 . Regression model checking . In Proceedings of ICSM. 115--124 . Guowei Yang, Matthew B. Dwyer, and Gregg Rothermel. 2009. Regression model checking. In Proceedings of ICSM. 115--124."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568319"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629536","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629536","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:18Z","timestamp":1750230078000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629536"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,7]]},"references-count":49,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,10,14]]}},"alternative-id":["10.1145\/2629536"],"URL":"https:\/\/doi.org\/10.1145\/2629536","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,7]]},"assertion":[{"value":"2013-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}