ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway

Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using monotonic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is unscalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection.

To address the above limitations, we present RecTopo a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs.

We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.

Mon 30 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:45
Formal Methods, Logics, and Static Analysis FrameworksTechnical Papers at Auditorium M003
Chair(s): Marco Carbone IT University of Copenhagen
11:00
21m
Talk
Compositional Static Value Analysis for Higher-Order Numerical Programs
Technical Papers
Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université
11:21
21m
Talk
Lightweight Diagramming for Formal Methods: A Grounded Language Design
Technical Papers
Siddhartha Prasad Brown University, Ben Greenman University of Utah, Tim Nelson Brown University, Shriram Krishnamurthi Brown University
11:42
21m
Talk
Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering
Technical Papers
Jiawei Yang , Xiao Cheng Macquarie University, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Xiapu Luo Hong Kong Polytechnic University, Yulei Sui University of New South Wales
12:03
21m
Talk
The Algebra of Patterns
Technical Papers
David Binder University of Kent, UK, Lean Ermantraut Radboud University Nijmegen
12:24
21m
Talk
A theory of (linear-time) timed monitors
Technical Papers
Mouloud Amara IRIF, Université Paris Cité, Giovanni Bernardi IRIF, Université Paris Cité, Mohammed Aristide Foughali Université Paris Cité / IRIF, Adrian Francalanza University of Malta
:
:
:
: