Verification by Abstract Interpretation

Patrick Cousot

Description

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

Sujets

• Abstract interpretation
• Abstraction

Informations

• Publié par: pefav
• Nombre de lectures: 12
• Langue: English

Extrait

1

Verification by Abstract Interpretation

Patrick Cousot

École normale supérieure, Département d’informatique
45 rue d’Ulm, 75230 Paris cedex 05, France
[e-mail],www.di.ens.fr/~cousot

6
Dedicated to Zohar Manna, for his2th birthday.

Abstract.Abstract interpretation theory formalizes the idea
ofabstractionof 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, which isrevisitedto handle infinitary abstractions,
and on the newparametric predicate abstraction.

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
concrete semantics of a programming language using an infinitary abstraction) and
on the newparametric predicate abstraction, a program-independent
generalization (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 Propertiesand 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).
Consequently, 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 latticehA,⊑,⊥,⊤,⊔,⊓i.
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 thatP⊑P. In theapproximation
from below,P∈ Ais under-approximated byP∈ Asuch thatP⊑P. Obviously
these notions are dual since an approximation from above/below for⊑/⊒is an
inverse approximation from below/above for⊒/⊑. 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⊤ ∈ Ato avoid that some concrete properties may have no
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 thatP⊑P
′ ′
and@P∈ A:P⊑PĹP. If, for economy, we would like to avoid trying all
possible minimal approximations, we can require that any concrete propertyP∈
′ ′′
Ahas abest abstractionP∈ A, that isP⊑Pand∀P∈ A:P⊑P⇒P⊑P
(otherwise see alternatives in [13]). By definition of the meet⊓, this hypothesis
is equivalent to the fact that the meet of abstract properties should be abstract
d d
′ ′′ ′
P={P∈ A |P⊑P} ∈ A(since otherwise{P∈ A |P⊑P}would have
no best abstraction).

2.2 MooreFamily-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
Δd
meet i.e.Mc(A) =Awhere theMoore-closureMc(X) ={S|S⊆X}is the
⊆-least Moore family containingAand the set imagef(X)of a setX⊆Dby
ΔT
a mapf∈D7→Eisf(X) ={f(x)|x∈X}. In particular∅=⊤ ∈ Aso
that any Moore family has a supremum. If the abstract domainAis a Moore
family of a complete latticehA,⊑,⊥,⊤,⊔,⊓ithen it is a complete meet
subsemilatticehA,⊑,⊓A,⊤, λS⊓{P∈ A | ⊔S⊆P},⊓iofA. The complete
∙
lattice of abstractionshMc(℘(A)),⊇,A,{⊤}, λSMc(∪S),∩iis the set of all
∙T
abstractions i.e. of Moore families on the setAof concrete properties.Aiis
i∈I
the most concrete among the abstract domains ofMc(℘(A))which are
abstracS
tions of all the abstract domains{Ai|i∈I} ⊆Mc(℘(A)).Mc(Ai)is the
i∈I
most abstract among the abstract domains ofMc(℘(A))which are more
concrete than all theAi’s and therefore isomorphic to thereduced product[11, Sec.
10.1]. Thedisjunctive completionof an abstract domainAis the most abstract
domainDc(A)=Mc({⊔X|X⊆ A})containing all concrete disjunctions of
the abstract properties ofA[11, Sec. 9.2].Ais disjunctive if and only ifDc(A)
=A.

2.3 ClosureOperator-Based Abstraction.The mapρmapping a
conA
crete propertyP∈ Ato its best abstractionρ(P)in the Moore familyAis
A