Shaurya Gomber | Searcharxiv

arXiv2025

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation

Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, causing three key limitations: transformers cannot be reused across domains; precise compositional reasoning over instruction sequences is difficult; and all downstream tasks must use the same fixed transformer regardless of precision or efficiency needs.To address this, we propose the Evolving Abstract Transformer, which replaces the fixed single-output design with an adaptable search over a parametric space of sound outputs via two algorithms. First, the Universal Parametric Output Space Encoder (UPOSE) constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators (QGO) class, covering both individual instructions and structured sequences. Second, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of UPOSE's output space to efficiently search it according to downstream objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate across three numerical abstract domains: Zones, Octagons, and Polyhedra. Results show the evolving transformer works across domains and instructions, enables efficient precision-efficiency tradeoffs by adjusting number of gradient steps in the search, and reaches the most precise invariants up to 3.2x faster than existing baselines.

cs.PL↗

arXiv2024

Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback

Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. However, the set of reachable program states is often unknown, and loop invariants are typically used to overapproximate it. So, proving the termination of a loop requires searching for both a ranking function and a loop invariant. Existing ranking function-based termination analysis techniques can be broadly categorized as (i) those that synthesize the ranking function and invariants independently, (ii) those that combine invariant synthesis with ranking function synthesis into a single query, and (iii) those that offer limited feedback from ranking function synthesis to guide invariant synthesis. These approaches either suffer from having too large a search space or inefficiently exploring the smaller, individual search spaces. In this work, we present a novel termination analysis framework Syndicate, which exploits bi-directional feedback to guide the searches for both ranking functions and invariants, increasing the number of programs that can be proven to terminate and reduces the average time needed to prove termination compared to baselines. Syndicate is general and allows different instantiations of templates, subprocedures, and parameters, offering users the flexibility to optimize the ranking function synthesis. Depending on the templates used, Syndicate is relatively complete and efficient, outperforming existing techniques that achieve at most one of these guarantees. Notably, despite a simpler approach compared to the baselines, Syndicate's performance is either comparable to or better than existing tools in terms of the number of benchmarks proved and average runtime.

cs.LO↗