2022/06/22 by Vincenzo Arceri, Arceri, Vincenzo, Isabella Mastroeni +3
Computer Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Software Engineering Research
paper · pdf · doi:10.48550/arxiv.2206.10893
openalex publication_date 2022/06/22 · openalex created_date 2022/06/25 · openalex updated_date 2026/07/28
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 A2I 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.