Decoupling the Ascending and Descending Phases in Abstract Interpretation
Abstract Interpretation approximates the semantics of a program by mimicking its concrete fixpoint computation on an abstract domain A. 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 A with a more precise abstract domain D. The correctness of the approach is justified by casting it as an instance of the A^2I 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 A and D.
Mon 5 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | Semantics and AnalysisAPLAS at Seminar Room G007 Chair(s): Julian Mackay Victoria University of Wellington | ||
10:30 30mTalk | An Algebraic Theory for Shared-State Concurrency APLAS File Attached | ||
11:00 30mTalk | Decoupling the Ascending and Descending Phases in Abstract Interpretation APLAS Vincenzo Arceri University of Parma, Italy, Isabella Mastroeni University of Verona, Italy, Enea Zaffanella University of Parma, Italy | ||
11:30 30mTalk | Inferring Region Types via an Abstract Notion of Environment Transformation APLAS |