{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:56Z","timestamp":1775873696597,"version":"3.50.1"},"reference-count":37,"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\/"}],"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>We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that consists of two distinct steps: computing a path expression that succinctly summarizes the set of program paths of interest, and interpreting the path expression using a properly-defined semantic algebra to obtain program properties of interest. In this context, the goal of an incremental algorithm is to reduce the analysis time by leveraging the intermediate results computed before the program changes. We have made two main contributions. First, we propose a data structure for efficiently representing path expression as a tree together with a tree-based interpreting method. Second, we propose techniques for efficiently updating the program properties in response to changes of the path expression. We have implemented our method and evaluated it on thirteen Java applications from the DaCapo benchmark suite. The experimental results show that both our method for incrementally computing path expression and our method for incrementally interpreting path expression are effective in speeding up the analysis. Compared to the baseline APA and two state-of-the-art APA methods, the speedup of our method ranges from 160\u00d7 to 4761\u00d7 depending on the types of program analyses performed.<\/jats:p>","DOI":"10.1145\/3704901","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1934-1961","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["An Incremental Algorithm for Algebraic Program Analysis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8493-6886","authenticated-orcid":false,"given":"Chenyu","family":"Zhou","sequence":"first","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4933-7443","authenticated-orcid":false,"given":"Yuzhou","family":"Fang","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5877-2677","authenticated-orcid":false,"given":"Jingbo","family":"Wang","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4684-3943","authenticated-orcid":false,"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2022. GnuPG Community. Libgcrypt. https:\/\/gnupg.org\/software\/libgcrypt\/index.html."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Tony Antoniadis Konstantinos Triantafyllou and Yannis Smaragdakis. 2017. Porting DOOP to Souffl\u00e9: A tale of Inter-engine Portability for Datalog-based Analyses. In ACM SIGPLAN International Workshop on State Of the Art in Program Analysis. ACM 25\u201330. https:\/\/doi.org\/10.1145\/3088515.3088522 10.1145\/3088515.3088522","DOI":"10.1145\/3088515.3088522"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Steven Arzt and Eric Bodden. 2014. Reviser: Efficiently Updating IDE-\/IFDS-based Data-flow Analyses in Response to Incremental Program Changes. In International Conference on Software Engineering. ACM 288\u2013298. https:\/\/doi.org\/10.1145\/2568225.2568243 10.1145\/2568225.2568243","DOI":"10.1145\/2568225.2568243"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Thomas Ball Rupak Majumdar Todd D. Millstein and Sriram K. Rajamani. 2001. Automatic Predicate Abstraction of C Programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM 203\u2013213. https:\/\/doi.org\/10.1145\/378795.378846 10.1145\/378795.378846","DOI":"10.1145\/378795.378846"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"S. M. Blackburn R. Garner C. Hoffman A. M. Khan K. S. McKinley R. Bentzur A. Diwan D. Feinberg D. Frampton S. Z. Guyer M. Hirzel A. Hosking M. Jump H. Lee J. E. B. Moss A. Phansalkar D. Stefanovi\u0107 T. VanDrunen D. von Dincklage and B. Wiedermann. 2006. The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In ACM SIGPLAN conference on Object-Oriented Programing Systems Languages and Applications. ACM 169\u2013190. https:\/\/doi.org\/10.1145\/1167473.1167488 10.1145\/1167473.1167488","DOI":"10.1145\/1167473.1167488"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622868"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In ACM Symposium on Principles of Programming Languages. ACM 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973 10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290358"},{"key":"e_1_3_2_10_2","unstructured":"Azadeh Farzan and Zachary Kincaid. 2013. An Algebraic Framework for Compositional Program Analysis. arXiv preprint arXiv:1310.3481 (2013)."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In International Conference on Formal Methods in Computer-Aided Design. IEEE 57\u201364. https:\/\/doi.org\/10.1109\/FMCAD.2015.7542253 10.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Gary A. Kildall. 1973. A Unified Approach to Global Program Optimization. In ACM Symposium on Principles of Programming Languages. ACM 194\u2013206. https:\/\/doi.org\/10.1145\/512927.512945 10.1145\/512927.512945","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid. 2018. Numerical Invariants via Abstract Machines. In Static Analysis - 25th International Symposium SAS 2018 Freiburg Germany August 29-31 2018 Proceedings. Springer 24\u201342. https:\/\/doi.org\/10.1007\/978-3-319-99725-4_3 10.1007\/978-3-319-99725-4_3","DOI":"10.1007\/978-3-319-99725-4_3"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158142"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Thomas W. Reps and John Cyphert. 2021. Algebraic Program Analysis. In Computer Aided Verification - 33rd International Conference CAV 2021 Virtual Event July 20-23 2021 Proceedings Part I (Lecture Notes in Computer Science Vol. 12759). Springer 46\u201383. https:\/\/doi.org\/10.1007\/978-3-030-81685-8_3 10.1007\/978-3-030-81685-8_3","DOI":"10.1007\/978-3-030-81685-8_3"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1990. On Kleene Algebras and Closed Semirings. In Mathematical Foundations of Computer Science. Springer 26\u201347. https:\/\/doi.org\/10.1007\/BFB0029594 10.1007\/BFB0029594","DOI":"10.1007\/BFB0029594"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Monica S. Lam John Whaley V. Benjamin Livshits Michael C. Martin Dzintars Avots Michael Carbin and Christopher Unkel. 2005. Context-sensitive Program Analysis as Database Queries. In ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems. ACM 1\u201312. https:\/\/doi.org\/10.1145\/1065167.1065169 10.1145\/1065167.1065169","DOI":"10.1145\/1065167.1065169"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Mayur Naik Alex Aiken and John Whaley. 2006. Effective Static Race Detection for Java. In ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM 308\u2013319. https:\/\/doi.org\/10.1145\/1133981.1134018 10.1145\/1133981.1134018","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Brandon Paulsen Chungha Sung Peter A. H. Peterson and Chao Wang. 2019. Debreach: Mitigating Compression Side Channels via Static Analysis and Transformation. In IEEE\/ACM International Conference on Automated Software Engineering. IEEE 899\u2013911. https:\/\/doi.org\/10.1109\/ASE.2019.00088 10.1109\/ASE.2019.00088","DOI":"10.1109\/ASE.2019.00088"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.58766"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00079-8"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Thomas W. Reps Emma Turetsky and Prathmesh Prabhu. 2016. Newtonian Program Analysis via Tensor Product. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM 663\u2013677. https:\/\/doi.org\/10.1145\/2837614.2837659 10.1145\/2837614.2837659","DOI":"10.1145\/2837614.2837659"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Barbara G. Ryder. 1983. Incremental Data Flow Analysis. In ACM Symposium on Principles of Programming Languages. ACM 167\u2013176. https:\/\/doi.org\/10.1145\/567067.567084 10.1145\/567067.567084","DOI":"10.1145\/567067.567084"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Chungha Sung Markus Kusano and Chao Wang. 2017. Modular Verification of Interrupt-driven Software. In IEEE\/ACM International Conference on Automated Software Engineering. IEEE 206\u2013216. https:\/\/doi.org\/10.1109\/ASE.2017.8115634 10.1109\/ASE.2017.8115634","DOI":"10.1109\/ASE.2017.8115634"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Chungha Sung Shuvendu K. Lahiri Constantin Enea and Chao Wang. 2018. Datalog-based Scalable Semantic Diffing of Concurrent Programs. In ACM\/IEEE International Conference on Automated Software Engineering. ACM 656\u2013666. https:\/\/doi.org\/10.1145\/3238147.3238211 10.1145\/3238147.3238211","DOI":"10.1145\/3238147.3238211"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Tam\u00e1s Szab\u00f3 Sebastian Erdweg and G\u00e1bor Bergmann. 2021. Incremental whole-program analysis in Datalog with lattices. In ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM 1\u201315. https:\/\/doi.org\/10.1145\/3453483.3454026 10.1145\/3453483.3454026","DOI":"10.1145\/3453483.3454026"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Tam\u00e1s Szab\u00f3 Sebastian Erdweg and Markus Voelter. 2016. IncA: a DSL for the definition of incremental program analyses. In IEEE\/ACM International Conference on Automated Software Engineering. ACM 320\u2013331. https:\/\/doi.org\/10.1145\/2970276.2970298 10.1145\/2970276.2970298","DOI":"10.1145\/2970276.2970298"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322272"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Di Wang Jan Hoffmann and Thomas W. Reps. 2018. PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM 513\u2013528. https:\/\/doi.org\/10.1145\/3192366.3192408 10.1145\/3192366.3192408","DOI":"10.1145\/3192366.3192408"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649822"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Jingbo Wang Chungha Sung Mukund Raghothaman and Chao Wang. 2021. Data-Driven Synthesis of Provably Sound Side Channel Analyses. In IEEE\/ACM International Conference on Software Engineering. IEEE 810\u2013822. https:\/\/doi.org\/10.1109\/ICSE43902.2021.00079 10.1109\/ICSE43902.2021.00079","DOI":"10.1109\/ICSE43902.2021.00079"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Jingbo Wang Chungha Sung and Chao Wang. 2019. Mitigating Power Side Channels during Compilation. In ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM 590\u2013601. https:\/\/doi.org\/10.1145\/3338906.3338913 10.1145\/3338906.3338913","DOI":"10.1145\/3338906.3338913"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"John Whaley and Monica S. Lam. 2004. Cloning-based Context-sensitive Pointer Alias Analysis using Binary Decision Diagrams. In ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation. ACM 131\u2013144. https:\/\/doi.org\/10.1145\/996841.996859 10.1145\/996841.996859","DOI":"10.1145\/996841.996859"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"David Zhao Pavle Subotic Mukund Raghothaman and Bernhard Scholz. 2021. Towards Elastic Incrementalization for Datalog. In International Symposium on Principles and Practice of Declarative Programming. ACM 20:1\u201320:16. https:\/\/doi.org\/10.1145\/3479394.3479415 10.1145\/3479394.3479415","DOI":"10.1145\/3479394.3479415"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Quan Zhou Sixuan Dang and Danfeng Zhang. 2024. CtChecker: A Precise Sound and Efficient Static Analysis for Constant-Time Programming. In European Conference on Object-Oriented Programming. 46:1\u201346:26. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2024.46 10.4230\/LIPICS.ECOOP.2024.46","DOI":"10.4230\/LIPICS.ECOOP.2024.46"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Shaowei Zhu and Zachary Kincaid. 2021. Termination Analysis without the Tears. In ACM SIGPLAN International Conference on Programming Language Design and Implementation. ACM 1296\u20131311. https:\/\/doi.org\/10.1145\/3453483.3454110 10.1145\/3453483.3454110","DOI":"10.1145\/3453483.3454110"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704901","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704901","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:24Z","timestamp":1770200244000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704901"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704901"],"URL":"https:\/\/doi.org\/10.1145\/3704901","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"}}]}}