{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:09:22Z","timestamp":1784200162143,"version":"3.55.0"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"Australian Research Grant","award":["DP250101396"],"award-info":[{"award-number":["DP250101396"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Abstract interpretation provides a systematic framework for static analysis, where widening operators are crucial for ensuring termination when analyzing programs over infinite-height lattices. Current abstract interpreters apply widening operations and fixpoint detection uniformly across all variables at the identified widening point (e.g., control-flow loop headers), leading to costly computations. Through our empirical study, we observe that infinite ascending chains typically originate from only a subset of variables involved in value-flow cycles, providing opportunities for selective widening and targeted fixpoint detection. This paper introduces an efficient approach to optimize abstract interpretation over non-relational domains through selective widening guided by value-flow analysis. We develop a modular and condensed value-flow graph (MVFG) that enables precise identification of variables requiring widening by detecting value-flow cycles across procedure boundaries. Our MVFG design incorporates efficient shortcut edges that summarize interprocedural value flows, achieving the precision of context-sensitive analysis but with linear complexity. By aligning value-flow cycles with the weak topological ordering (WTO) of the control-flow graph, we identify the minimal set of variables requiring widening operations, applying widening exclusively to variables that participate in value-flow back edges. Our evaluation on large-scale open-source projects shows that our selective widening approach reduces analysis time by up to 41.2% while maintaining identical precision. The method significantly reduces the number of widened variables by up to 99.5%, with greater benefits observed in larger codebases.<\/jats:p>","DOI":"10.1145\/3763083","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"922-949","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Abstract Interpretation via Selective Widening"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-0582-5966","authenticated-orcid":false,"given":"Jiawei","family":"Wang","sequence":"first","affiliation":[{"name":"UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5456-3827","authenticated-orcid":false,"given":"Xiao","family":"Cheng","sequence":"additional","affiliation":[{"name":"Macquarie University, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9510-6574","authenticated-orcid":false,"given":"Yulei","family":"Sui","sequence":"additional","affiliation":[{"name":"UNSW, Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2023. bc - An arbitrary precision calculator language. https:\/\/www.gnu.org\/software\/bc\/"},{"key":"e_1_3_1_3_1","unstructured":"2023. curl - A command line tool and library for transferring data with URLs. https:\/\/curl.se\/"},{"key":"e_1_3_1_4_1","unstructured":"2023. gzip - GNU compression utility. https:\/\/www.gnu.org\/sofrware\/gzip\/"},{"key":"e_1_3_1_5_1","unstructured":"2023. htop - An interactive process viewer for Unix systems. https:\/\/htop.dev\/"},{"key":"e_1_3_1_6_1","unstructured":"2023. md5sum - A utility to generate and verify MD5 checksums. https:\/\/www.gnu.org\/software\/coreutils\/manual\/html_node\/md5sum-invocation.html"},{"key":"e_1_3_1_7_1","unstructured":"2023. OpenSSL - A robust full-featured open-source toolkit for SSL and TLS. https:\/\/www.openssl.org\/"},{"key":"e_1_3_1_8_1","unstructured":"2023. Redis - The open source in-memory data store used by millions of developers as a database cache streaming engine and message broker. https:\/\/github.com\/redis\/redis\/"},{"key":"e_1_3_1_9_1","unstructured":"2023. Teeworlds - A retro multiplayer shooter. https:\/\/teeworlds.com\/"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_4"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.12.005"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.003"},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","unstructured":"George Balatsouras and Yannis Smaragdakis. 2016. Structure-Sensitive Points-To Analysis for C and C++. In SAS \u201916.","DOI":"10.1007\/978-3-662-53413-7_5"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO51591.2021.9370334"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Bruno Blanchet Patrick Cousot Radhia Cousot J\u00e9r\u00f4me Feret Laurent Mauborgne Antoine Min\u00e9 David Monniaux and Xavier Rival. 2003. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation. 196\u2013207.","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039704"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_20"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10431-7_20"},{"key":"e_1_3_1_19_1","doi-asserted-by":"crossref","unstructured":"Xavier RivalBor-Yuh Evan Chang. 2011. Calling Context Abstraction with Shapes. 173\u2013186.","DOI":"10.1145\/1926385.1926406"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_21"},{"key":"e_1_3_1_21_1","doi-asserted-by":"crossref","unstructured":"Xiao Cheng Haoyu Wang Jiayi Hua Guoai Xu and Yulei Sui. 2021. DeepWukong: Statically Detecting Software Vulnerabilities Using Deep Graph Neural Network. ACM Trans. Softw. Eng. Methodol. (2021).","DOI":"10.1145\/3436877"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639220"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534371"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61053-7_66"},{"key":"e_1_3_1_25_1","unstructured":"clam. 2024. Clam: LLVM front-end for Crab. https:\/\/github.com\/seahorn\/clam."},{"key":"e_1_3_1_26_1","first-page":"303","volume-title":"Program flow analysis: theory and applications","author":"Cousot Patrick","year":"1981","unstructured":"Patrick Cousot. 1981. Semantic foundations of program analysis. In Program flow analysis: theory and applications. Prentice Hall, 303\u2013342."},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"e_1_3_1_30_1","volume-title":"Proceedings of the ACM on Programming Languages","author":"Cousot Patrick","year":"2019","unstructured":"Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato. 2019a. A2I: abstract2 interpretation. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1\u201331."},{"key":"e_1_3_1_31_1","first-page":"31","volume-title":"Proc. ACM Program. Lang.","author":"Cousot Patrick","year":"2019","unstructured":"Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato. 2019b. A2I: Abstract2 Interpretation. Proc. ACM Program. Lang. 3, POPL, Article 42 (jan 2019), 31 pages."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512538"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_41"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-95561-8_8"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008678014487"},{"key":"e_1_3_1_37_1","first-page":"289","article-title":"Flow-sensitive pointer analysis for millions of lines of code","author":"Hardekopf B.","year":"2011","unstructured":"B. Hardekopf and C. Lin. 2011. Flow-sensitive pointer analysis for millions of lines of code. CGO \u201911 (2011), 289\u2013298.","journal-title":"CGO \u201911"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_12"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2381"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498718"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Yuxiang Lei Yulei Sui Shin Hwei Tan and Qirun Zhang. 2023. Recursive State Machine Guided Graph Folding for Context-Free Language Reachability. Proc. ACM Program. Lang. Article 119 (2023). https:\/\/doi.org\/10.1145\/3591233 10.1145\/3591233","DOI":"10.1145\/3591233"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11688839_5"},{"key":"e_1_3_1_43_1","first-page":"201","volume-title":"Static Analysis","author":"Madsen Magnus","year":"2014","unstructured":"Magnus Madsen and Anders M\u00f8ller. 2014. Sparse Dataflow Analysis with Pointers and Reachability. In Static Analysis, Markus M\u00fcller-Olm and Helmut Seidl (Eds.). Springer International Publishing, Cham, 201\u2013218."},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590811"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254092"},{"key":"e_1_3_1_46_1","unstructured":"Hakjoo Oh Kihong Heo Wonchan Lee Woosuk Lee and Kwangkeun Yi. 2012b. The Sparrow static analyzer. https:\/\/opam.ocaml.org\/packages\/sparrow\/."},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2821504"},{"key":"e_1_3_1_48_1","unstructured":"OpenCV. 2023. OpenCV Contrib: Extra modules for OpenCV. https:\/\/github.com\/opencv\/opencv_contrib. GitHub repository."},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179497"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302516.3307349"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1290520.1290524"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512961"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199462"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192418"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454086"},{"key":"e_1_3_1_57_1","doi-asserted-by":"crossref","unstructured":"Benno Stein Bor-Yuh Evan Chang and Manu Sridharan. 2021. Demanded abstract interpretation. In PLDI.","DOI":"10.1145\/3453483.3454044"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3648441"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428301"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892235"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336784"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2302311"},{"key":"e_1_3_1_63_1","doi-asserted-by":"crossref","unstructured":"Yulei Sui Sen Ye Jingling Xue and Pen-Chung Yew. 2011. SPAS: Scalable Path-Sensitive Pointer Analysis on Full-Sparse SSA. Programming Languages and Systems (APLAS \u201911) (2011) 155\u2013171.","DOI":"10.1007\/978-3-642-25318-8_14"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_24"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_3_1_66_1","doi-asserted-by":"crossref","unstructured":"Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. (1955).","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_1_67_1","first-page":"12","volume-title":"Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering (Rochester, MI, USA) (ASE \u201922)","author":"Veileborg Oskar Haarklou","year":"2023","unstructured":"Oskar Haarklou Veileborg, Georgian-Vlad Saioc, and Anders M\u00f8ller. 2023. Detecting Blocking Errors in Go Programs Using Localized Abstract Interpretation. 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 32, 12 pages."},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179479"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/103135.103136"},{"key":"e_1_3_1_70_1","doi-asserted-by":"crossref","unstructured":"Cathrin Weiss Cindy Rubio-Gonz\u00e1lez and Ben Liblit. 2015. Database-Backed Program Analysis for Scalable Error Propagation. In 2015 IEEE\/ACM 37th IEEE International Conference on Software Engineering Vol. 1. 586\u2013597.","DOI":"10.1109\/ICSE.2015.75"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2025.34"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485495"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1772954.1772985"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303972"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763083","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:11:22Z","timestamp":1784196682000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763083"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":73,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763083"],"URL":"https:\/\/doi.org\/10.1145\/3763083","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}