BASIC CONCEPTS OF ABSTRACT INTERPRETATION

Patrick Cousot

Description

Niveau: Supérieur, Doctorat, Bac+8
BASIC CONCEPTS OF ABSTRACT INTERPRETATION Patrick Cousot École Normale Supérieure 45 rue d'Ulm 75230 Paris cedex 05, France Radhia Cousot CNRS & École Polytechnique 91128 Palaiseau cedex, France Abstract A brief introduction to the theory of Abstract Interpretation, examplified by constructing a hierarchy of partial traces, reflexive transitive closure, reachable states and intervals abstract semantics of transition systems. Keywords: Abstract Interpretation, Safety, Specification, Static Analysis, Verification. 1. Introduction Abstract Interpretation [Cousot, 1978] is a theory of approximation of math- ematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science such that the semantics, the proof, the static analysis, the verification, the safety and the security of soft- ware or hardware computer systems. In particular, static analysis by abstract interpretation, which automatically infers dynamic properties of computer sys- tems, has been very successful these last years to automatically verify complex properties of real-time, safety-critical embedded systems. All applications presented in the WCC 2004 topical day on Abstract In- terpretation compute an overapproximation of the program reachable states. Hence, we consisely develop the elementary example of reachability static analysis [Cousot and Cousot, 1977].

• ?i ?


• all finite


• ?i


• transition systems


• partial trace


• n≥0 ?n?


• ?s ?


• semantics


• ?n? ?

Sujets

• École polytechnique
• Partial trace
• Semantics

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 17
• Langue: English

Extrait

ABABSSITCRCACOTNICNETPETRSPORFETATION

PatrickCousot
ÉcoleNormaleSupérieure
45rued’Ulm
75230Pariscedex05,France
[e-mail]

RadhiaCousot
9C1N1R28SP&alÉacisoeleauPocleydteexc,hnFirqaunece
[e-mail]

Abstract
AbriefintroductiontothetheoryofAbstractInterpretation,exampli
fi
edby
constructingahierarchyofpartialtraces,re
fl
exivetransitiveclosure,reachable
statesandintervalsabstractsemanticsoftransitionsystems.
Keywords:
AbstractInterpretation,Safety,Speci
fi
cation,StaticAnalysis,Veri
fi
cation.
1.Introduction
AbstractInterpretation[Cousot,1978]isatheoryofapproximationofmath-
ematicalstructures,inparticularthoseinvolvedinthesemanticmodelsof
computersystems.Abstractinterpretationcanbeappliedtothesystematic
constructionofmethodsandeffectivealgorithmstoapproximateundecidable
orverycomplexproblemsincomputersciencesuchthatthesemantics,the
proof,thestaticanalysis,theveri
fi
cation,thesafetyandthesecurityofsoft-
wareorhardwarecomputersystems.Inparticular,staticanalysisbyabstract
interpretation,whichautomaticallyinfersdynamicpropertiesofcomputersys-
tems,hasbeenverysuccessfultheselastyearstoautomaticallyverifycomplex
propertiesofreal-time,safety-criticalembeddedsystems.
AllapplicationspresentedintheWCC2004topicaldayonAbstractIn-
terpretationcomputeanoverapproximationoftheprogramreachablestates.
Hence,weconsiselydeveloptheelementaryexampleofreachabilitystatic
analysis[CousotandCousot,1977].Welimitthenecessarymathematical
conceptstonaïvesettheory.Amorecompletepresentationis[Cousot,2000a]
while[Cousot,1981;CousotandCousot,1992b]canberecommendedas
fi
rst
readingsand[CousotandCousot,1992a]forabasicexpositiontothetheory.

2
BasicConceptsofAbstractInterpretation
2.Transitionsystems
Programsareoftenformalizedasgraphsortransitionsystems
τ
=

Σ
,
Σ
i
,
t

where
Σ
isasetofstates,
Σ
i
⊆
Σ
isthesetofinitialstatesand
t
⊆
Σ
×
Σ
isatransitionrelationbetweenastateanditspossiblesuccessors[Cousot,
1978;Cousot,1981].Forexampletheprogram
x:=0;whilex<100
dox:=x+1
canbeformalizedas

Z
,
{
0
}
,
{
x,x

|
x<
100
∧
x

=
x
+1
}
where
Z
isthesetofintegers.
3.Partialtracesemantics
A
fi
nitepartialexecutiontrace
s
0
s
1
...s
n
startsfromanystate
s
0
∈
Σ
and
thenmovesonthroughtransitionsfromonestate
s
i
,
i<n
,toapossiblesuc-
cessor
s
i
+1
suchthat

s
i
,s
i
+1
∈
t
.Thesetofallsuch
fi
nitepartialexecution
traceswillbecalledthe
collectingsemantics
Σ
τ
∗
ofthetransitionsysteminthat
itisthestrongestprogrampropertyofinterest(inthispaper).
Thereisnopartialtraceoflength0sotheset
Σ
τ
0
ofpartialtracesoflength
0issimplytheemptyset
∅
.Apartialtraceoflength1is
s
where
s
∈
Σ
is
anystate.Sotheset
Σ
τ
1
ofpartialtracesoflength1issimply
{
s
|
s
∈
Σ
}
.
Byrecurrence,atraceoflength
n
+1
istheconcatenation
σss

ofatrace
σs
oflength
n
withapartialtrace
s

oflength1suchthatthepair

s,s

∈
t
is
apossiblestatetransition.Soif
Σ
τn
isthesetofpartialtracesoflength
n
then
Σ
τn
+1
=
{
σss

|
σs
∈
Σ
τn
∧
s,s

∈
t
}
.Thenthecollectingsemanticsof
τ
is
theset
Σ
τ
∗
=
n
≥
0
Σ
τn
ofallpartialtracesofall
fi
nitelengths.
4.Partialtracesemanticsin
fi
xpointform
Observethat
Σ
τ
1
∪
Σ
τn
+1
=
F
τ
∗
(Σ
τn
)
where:
F
τ
∗
(
X
)=
{
s
|
s
∈
Σ
}∪{
σss

|
σs
∈
X
∧
s,s

∈
t
sothat
Σ
τ
∗
isa
fi
xpoint
of
F
τ
∗
inthat
F
τ
∗
(Σ
τ
∗
)
=
Σ
τ
∗
[CousotandCousot,1979].
Theproofisasfollows:
F
τ
∗
(Σ
τ
∗
)=
F
τ
∗
(Σ
τn
)

bydef.
Σ
τ
∗

0n≥=
{
s
|
s
∈
Σ
}∪{
σss

|
σs
∈
(Σ
τn
)
∧
s,s

∈
t
}

def.
F
τ
∗

0n≥=
{
s
|
s
∈
Σ
}∪{
σss

|
σs
∈
Σ
τn
∧
s,s

∈
t
}

settheory
0n≥=
Σ
τ
1
∪
Σ
τn
+1

bydef.
Σ
τ
1
and
Σ
τn
+1

n
≥

0

=
Σ
τn
=Σ
τn

byletting
n

=
n
+1
andsince
Σ
τn
=
∅
.

n

≥
1
n
≥
0

}
PatrickCousot&RadhiaCousot
3
Nowassumethat
F
τ
∗
(
X
)=
X
isanother
fi
xpointof
F
τ
∗
.Weproveby
recurrencethat
∀
n
≥
0:Σ
τn
⊆
X
.Obviously
Σ
τ
0
=
∅⊆
X
.
Σ
τ
1
=
{
s
|
s
∈
Σ
}⊆F
τ
∗
(
X
)
=
X
.Assumebyrecurrencehypothesisthat
Σ
τn
⊆
X
.
Then
σs
∈
Σ
τn
implies
σs
∈
X
so
{
σss

|
σs
∈
Σ
τn
∧
s,s

∈
t
}⊆
{
σss

|
σs
∈
X
∧
s,s

∈
t
}
whence
Σ
τn
+1
⊆F
τ
∗
(Σ
τn
)
⊆F
τ
∗
(
X
)=
X
.By
recurrence
∀
n
≥
0:Σ
τn
⊆
X
whence
Σ
τ
∗
isthe
least
fi
xpoint
of
F
τ
∗
,written:
Σ
τ
∗
=lfp
⊆
F
τ
∗
=
F
τ
∗
n
(
∅
)
∅0n≥where
f
0
(
x
)=
x
and
f
n
+1
(
x
)=
f
(
f
n
(
x
))
arethe
iterates
of
f
.
5.There
fl
exivetransitiveclosureasanabstractionofthe
partialtracesemantics
Partialexecutiontracesaretooprecisetoexpressprogrampropertiesthat
donotrelatetointermediatecomputationsteps.Consideringinitialand
fi
nal
statesonlyisanabstraction:
α
∗
(
X
)=
{
α
(
σ
)
|
σ
∈
X
}
where
α
(
s
0
s
1
...s
n
)=

s
0
,s
n

.
Observethat
α
∗
(Σ
τ
∗
)
isthere
fl
exivetransitiveclosure
t
∗
ofthetransitionrela-
tion
t
viz.thesetofpair

s,s


suchthatthereisa
fi
nitepathinthegraph
τ
=

Σ
,
Σ
i
,t

fromvertex
s
tovertex
s

througharcsof
t
:

x,y
∈
t
∗
ifandonly
if
∃
s
0
,...,s
n
∈
Σ:
x
=
s
0
∧
...
∧
s
i
,s
i
+1
∈
t
∧
...
∧
s
n
=
y
.
Nowif
Y
isasetofpairsofinitialand
fi
nalstates,itdescribesasetofpartial
traceswheretheintermediatestatesareunkown:
γ
∗
(
Y
)=
{
σ
|
^