Comparing the Galois Connection and Widening Narrowing Approaches

Niveau: Supérieur
Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation Patrick Cousot1 and Radhia Cousot2 1 LIENS, DMI, École Normale Supérieure, 45, rue d'Ulm, 75230 Paris cedex 05 (France) 2 LIX, École Polytechnique, 91128 Palaiseau cedex (France) Abstract. The use of infinite abstract domains with widening and - narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach re? stricted to finite lattices (or lattices satisfying the chain condition). 1 Introduction A widely-held opinion is that finite lattices (or lattices satisfying the chain condi? tion, i.e., such that all strictly increasing chains are finite) can be used instead of widenings and narrowings to ensure the termination of abstract interpretations of programs on infinite lattices. We show that, in general, this can only be to the detriment of precision and prove that the use of infinite abstract domains with widenings and narrowings is more powerful than the Galois connection approach for finite lattices (or lattices satisfying the chain condition). By way of example, various widenings are suggested for solving non-convergence problems left open in the literature. 2 Upper Approximation of the Collecting Semantics Following [CC76,CC77a,CC79b] , the abstract interpretation of a program can be formalized as the e?ective computation of an upper approximation A of the collecting semantics of the program.

• abstract interpretation


• con?? ?


• precise than


• strictly nec?


• approximation relation


• no strictly


• galois connection


• upper approximation