Decoupling the ascending and descending phases in abstract interpretation

DOI10.1007/978-3-031-21037-2_2zbMATH1524.68072OpenAlexW4312607842MaRDI QIDQ6176563FDOQ6176563

Authors Vincenzo Arceri, Isabella Mastroeni, Enea Zaffanella

Publication date 25 July 2023

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

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

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)

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$.

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

Cites work

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

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)