SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 16:30 - 16:45 at Orchid East - Abstraction Chair(s): Steve Blackburn

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.

Sat 18 Oct

Displayed time zone: Perth change

16:00 - 17:30
AbstractionOOPSLA at Orchid East
Chair(s): Steve Blackburn Google and Australian National University
16:00
15m
Talk
Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
OOPSLA
Mihai Nicola Stevens Institute of Technology, Chaitanya Agarwal New York University, Eric Koskinen Stevens Institute of Technology, Thomas Wies New York University
16:15
15m
Talk
A Hoare Logic For Symmetry Properties
OOPSLA
Vaibhav Mehta Cornell University, Justin Hsu Cornell University
16:30
15m
Talk
Efficient Abstract Interpretation via Selective Widening
OOPSLA
Jiawei Wang UNSW, Xiao Cheng Macquarie University, Yulei Sui University of New South Wales
16:45
15m
Talk
Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic
OOPSLA
Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University
17:00
15m
Talk
Structural Abstraction and Refinement for Probabilistic Programs
OOPSLA
Guanyan Li University of Oxford, Juanen Li Beijing Normal University, Zhilei Han Tsinghua University, Peixin Wang East China Normal University, Hongfei Fu Shanghai Jiao Tong University, Fei He Tsinghua University
17:15
15m
Talk
Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
OOPSLA
Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google