Decoupling the ascending and descending phases in abstract interpretation

DOI10.1007/978-3-031-21037-2_2zbMATH Open1524.68072arXiv2206.10893OpenAlexW4312607842MaRDI QIDQ6176563FDOQ6176563

Authors: Vincenzo Arceri, Isabella Mastroeni, Enea Zaffanella 

Publication date: 25 July 2023

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: Abstract Interpretation approximates the semantics of a program by mimicking its concrete fixpoint computation on an abstract domain $mathbbA$. The abstract (post-) fixpoint computation is classically divided into two phases: the ascending phase, using widenings as extrapolation operators to enforce termination, is followed by a descending phase, using narrowings as interpolation operators, so as to mitigate the effect of the precision losses introduced by widenings. In this paper we propose a simple variation of this classical approach where, to more effectively recover precision, we decouple the two phases: in particular, before starting the descending phase, we replace the domain $mathbbA$ with a more precise abstract domain $mathbbD$. The correctness of the approach is justified by casting it as an instance of the A${}^2$I framework. After demonstrating the new technique on a simple example, we summarize the results of a preliminary experimental evaluation, showing that it is able to obtain significant precision improvements for several choices of the domains $mathbbA$ and $mathbbD$.

Full work available at URL: https://arxiv.org/abs/2206.10893

Recommendations

• Narrowing operators on template abstract domains
• Descending chains and narrowing on template abstract domains
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Refining abstract interpretations
• Dissecting widening: separating termination from information

zbMATH Keywords

abstract interpretationstatic analysisnarrowingwidening

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• Combining Widening and Acceleration in Linear Relation Analysis
• The octagon abstract domain
• Fast polyhedra abstract domain
• Title not available (Why is that?)
• Precise widening operators for convex polyhedra
• Abstract interpretation and application to logic programs
• Systematic design of program transformation frameworks by abstract interpretation
• Static Analysis by Policy Iteration on Relational Domains
• Precise Fixpoint Computation Through Strategy Iteration
• Guided Static Analysis
• Abstract Interpretation Frameworks
• Widening Polyhedra with Landmarks
• On collecting semantics for program analysis
• Some ways to reduce the space dimension in polyhedra computations
• Verification, Model Checking, and Abstract Interpretation
• PPLite: zero-overhead encoding of NNC polyhedra
• Improving the results of program analysis by abstract interpretation beyond the decreasing sequence
• Stratified static analysis based on variable dependencies
• Descending chains and narrowing on template abstract domains
• Program analysis is harder than verification: a computability perspective
• An efficient abstract domain for not necessarily closed polyhedra
• A direct encoding for NNC polyhedra

This page was built for publication: Decoupling the ascending and descending phases in abstract interpretation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6176563)