//img.uscri.be/pth/2810a4b7c88b864348fb21c2e4126a30898a02c5
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Verification by Abstract Interpretation

De
25 pages
Verification by Abstract Interpretation Patrick Cousot École normale supérieure, Département d'informatique 45 rue d'Ulm, 75230 Paris cedex 05, France , Dedicated to Zohar Manna, for his 26th birthday. Abstract. Abstract interpretation theory formalizes the idea of abstrac- tion of mathematical structures, in particular those involved in the spec- ification of properties and proof methods of computer systems. Verifica- tion by abstract interpretation is illustrated on the particular cases of predicate abstraction, which is revisited to handle infinitary abstractions, and on the new parametric predicate abstraction. 1 Introduction Abstract interpretation theory [7,8,9,11,13] formalizes the idea of abstraction of mathematical structures, in particular those involved in the specification of properties and proof methods of computer systems. Verification by abstract interpretation is illustrated on the particular cases of predicate abstraction [4,15,19] (where the finitary program-specific ground atomic propositional components of inductive invariants have to be provided) which is revisited (in that it is derived by systematic approximation of the con- crete semantics of a programming language using an infinitary abstraction) and on the new parametric predicate abstraction, a program-independent generaliza- tion (where parameterized infinitary predicates are automatically combined by reduction and instantiated to particular programs by approximation).

  • abstract domains

  • such finite

  • abstract interpretation

  • abstraction

  • abstraction ?

  • concrete property

  • galois connection-based

  • all such

  • domains can


Voir plus Voir moins
Verification by Abstract Interpretation
Patrick Cousot
École normale supérieure, Département d’informatique 45 rue d’Ulm, 75230 Paris cedex 05, France cousot@ens.fr,uoc~tos.ens.fr/www.di Dedicated to Zohar Manna, for his26th birthday.
Abstract.Abstract interpretation theory formalizes the idea ofabstrac-tionof mathematical structures, in particular those involved in the spec-ification of properties and proof methods of computer systems. Verifica-tion by abstract interpretation is illustrated on the particular cases of predicate abstraction, which isrevisitedto handle infinitary abstractions, and on the newparametric predicate abstraction.
1 Introduction
Abstract interpretation theory [7,8,9,11,13] formalizes the idea ofabstraction of mathematical structures, in particular those involved in the specification of properties and proof methods of computer systems. Verification by abstract interpretation is illustrated on the particular cases ofpredicate abstraction[4,15,19] (where the finitary program-specific ground atomic propositional components of inductive invariants have to be provided) which isrevisited(in that it is derived by systematic approximation of the con-crete semantics of a programming language using an infinitary abstraction) and on the newparametric predicate abstraction, a program-independent generaliza-tion (where parameterized infinitary predicates are automatically combined by reduction and instantiated to particular programs by approximation).
2 Elements of Abstract Interpretation
Let us first recall a few elements of abstract interpretation from [7,9,11].
2.1 Properties and Their Abstraction.Given a setΣof objects (such as program states, execution traces, etc.), we represent propertiesPof objects sΣas sets of objectsP(Σ)(which have the considered property). Conse-quently, the set of properties of objects inΣis a complete Boolean latticeh(Σ) Σ¬i. More generally, and up to an encoding, the object properties are assumed to belong to a complete latticehAv>tui. By “abstraction”, we understand a reasoning or (mechanical) computation on objects such that only some of the properties of these objects can be used. Let us callconcretethe general properties inA. LetA ⊆ Abe the set ofabstract
properties that can be used in the reasoning or computation. So, abstraction consists inapproximatingthe concrete properties by the abstract ones. There are two possible directions of approximation. In theapproximation from above, P∈ Ais over-approximated byP∈ Asuch thatPvP. In theapproximation from below,P∈ Ais under-approximated by∈ Asuch thatvP. Obviously these notions are dual since an approximation from above/below forv/wis an inverse approximation from below/above forw/v. Moreover, the complement dual of an approximation from above/below forPis an approximation from below/above for¬P. Therefore, from a purely mathematical point of view, only approximations from above need to be presented. We require> ∈ Athat some concrete properties may have noto avoid abstraction (e.g. whenA=). Hence any concrete propertyP∈ Acan always be approximated from above (by>i.e.Σ, “true” or “I don’t know”). For best precision we want to useminimal abstractionsP∈ A, if any, such thatPvP andP0∈ A:PvP0ĹP. If, for economy, we would like to avoid trying all possible minimal approximations, we can require that any concrete propertyPAhas abest abstractionP∈ A, that isPvPandP0∈ A:PvP0PvP0 (otherwise see alternatives in [13]). By definition of the meetu, this hypothesis is equivalent to the fact that the meet of abstract properties should be abstract P=dP0∈ A |PvP0} ∈ A(since otherwisedP0∈ A |PvP0}would have no best abstraction).
2.2 Moore Family-Based Abstraction.The hypothesis that any concrete propertyP∈ Ahas abest abstractionP∈ Aimplies that the setAof abstract properties is aMoore family[11, Sec. 5.1] that is, by definition,Ais closed under meet i.e.McA) =Awhere theMoore-closureMc(X) =Δ{dS|SX}is the -least Moore family containingAand the set imagef(X)of a setXDby a mapfD7→Eisf(X) =Δ{f(x)|xX}. In particularT=> ∈ Aso that any Moore family has a supremum. If the abstract domainAis a Moore family of a complete latticehAv>tuithen it is a complete meet sub-semilatticeAvA> λSuP∈ A | tSP}uiofA. The complete lattice of abstractionshMc((A))A{>} λSMc(S)∩iis the set of all abstractions i.e. of Moore families on the setAof concrete properties.TiIAiis the most concrete among the abstract domains ofMc((A))which are abstrac-tions of all the abstract domainsAi|iI} ⊆Mc((A)).Mc(SiIAi)is the most abstract among the abstract domains ofMc((A))which are more con-crete than all theAi’s and therefore isomorphic to thereduced product[11, Sec. 10.1]. Thedisjunctive completionof an abstract domainAis the most abstract domainDcA)=Mc({tX|X⊆ A})containing all concrete disjunctions of the abstract properties ofA[11, Sec. 9.2].Ais disjunctive if and only ifDcA) =A.
2.3 Closure Operator-Based Abstraction.The mapAmapping a con-crete propertyP∈ Ato its best abstractionA(P)in the Moore familyAis