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

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)