Abstract Interpretation and Application to Logic Programs

Niveau: Supérieur
Abstract Interpretation and Application to Logic Programs ? Patrick Cousot LIENS, École Normale Supérieure 45, rue d'Ulm 75230 Paris cedex 05 (France) Radhia Cousot LIX, École Polytechnique 91128 Palaiseau cedex (France) Abstract. Abstract interpretation is a theory of semantics approximation which is used for the con? struction of semantics-based program analysis algorithms (sometimes called “data flow analysis”), the comparison of formal semantics (e.g., construction of a denotational semantics from an operational one), the design of proof methods, etc. Automatic program analysers are used for determining statically conservative approximations of dy? namic properties of programs. Such properties of the run-time behavior of programs are useful for debug? ging (e.g., type inference), code optimization (e.g., compile-time garbage collection, useless occur-check elimination), program transformation (e.g., partial evaluation, parallelization), and even program cor? rectness proofs (e.g., termination proof). After a few simple introductory examples, we recall the classical framework for abstract interpretation of programs. Starting from a standard operational semantics formalized as a transition system, classes of program properties are first encapsulated in collecting semantics expressed as fixpoints on partial orders representing concrete program properties.

• abstract interpretation


• upon


• operational semantics


• run-time behavior


• program anoldlookatoptimizingarrayboundchecking


• methods based


• partial order


• upon initialization