8 Pages
English

BASIC CONCEPTS OF ABSTRACT INTERPRETATION

-

Gain access to the library to view online
Learn more

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? ?


Subjects

Informations

Published by
Reads 17
Language English

ABABSSITCRCACOTNICNETPETRSPORFETATION

PatrickCousot
ÉcoleNormaleSupérieure
45rued’Ulm
75230Pariscedex05,France
Patrick.Cousot@ens.fr

RadhiaCousot
9C1N1R28SP&alÉacisoeleauPocleydteexc,hnFirqaunece
Radhia.Cousot@polytechnique.fr

Abstract
AbriefintroductiontothetheoryofAbstractInterpretation,exampli

edby
constructingahierarchyofpartialtraces,re

exivetransitiveclosure,reachable
statesandintervalsabstractsemanticsoftransitionsystems.
Keywords:
AbstractInterpretation,Safety,Speci

cation,StaticAnalysis,Veri

cation.
1.Introduction
AbstractInterpretation[Cousot,1978]isatheoryofapproximationofmath-
ematicalstructures,inparticularthoseinvolvedinthesemanticmodelsof
computersystems.Abstractinterpretationcanbeappliedtothesystematic
constructionofmethodsandeffectivealgorithmstoapproximateundecidable
orverycomplexproblemsincomputersciencesuchthatthesemantics,the
proof,thestaticanalysis,theveri

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

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

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

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

nitelengths.
4.Partialtracesemanticsin

xpointform
Observethat
Σ
τ
1

Σ
τn
+1
=
F
τ


τn
)
where:
F
τ

(
X
)=
{
s
|
s

Σ
}∪{
σss

|
σs

X

s,s


t
sothat
Σ
τ

isa

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

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

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

exivetransitiveclosureasanabstractionofthe
partialtracesemantics
Partialexecutiontracesaretooprecisetoexpressprogrampropertiesthat
donotrelatetointermediatecomputationsteps.Consideringinitialand

nal
statesonlyisanabstraction:
α

(
X
)=
{
α
(
σ
)
|
σ

X
}
where
α
(
s
0
s
1
...s
n
)=

s
0
,s
n

.
Observethat
α


τ

)
isthere

exivetransitiveclosure
t

ofthetransitionrela-
tion
t
viz.thesetofpair

s,s


suchthatthereisa

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

nalstates,itdescribesasetofpartial
traceswheretheintermediatestatesareunkown:
γ

(
Y
)=
{
σ
|
α
(
σ
)

Y
}
=
{
s
0
s
1
...s
n
|
s
0
,s
n

Y
}
Soif
X
isasetofpartialtraces,itisapproximatedfromaboveby
α

(
X
)
in
thesensethat
X

γ

(
α

(
X
))
.
6.Answeringconcretequestionsintheabstract
Toanswerconcretequestionsabout
X
onemaysometimesansweritusing
asimplerabstractquestionon
α

(
X
)
.Forexampletheconcretequestion“Is
thereapartialtraceinXwhichhas
s
,
s

and
s

asinitial,intermediateand

nalstates?”canbereplacedbytheabstractquestion“Isthereapair

s,s


in
α

(
X
)
?”.Ifthereisnosuchapairin
α

(
X
)
thenthereisnosuchapartialtrace
in
γ

(
α

(
X
))
whencenonein
X
since
X

γ

(
α

(
X
))
.Howeverifthereis
suchapairin
α

(
X
)
thenwecannotconcludethatthereissuchatracein
X
sincethistracemightbein
γ

(
α

(
X
))
butnotin
X
.Theabstractanswermust
alwaysbesoundbutmaysometimesbeincomplete.Howeveriftheconcrete
questionis“IsthereapartialtraceinXwhichhasrespectively
s
and
s

as
initialand

nalstates?”thentheabstractanswerissoundandcomplete.

4
BasicConceptsofAbstractInterpretation
7.Galoisconnections
Givenanyset
X
ofpartialtracesand
Y
ofpairofstates,wehave:
α

(
X
)

Y
⇐⇒{
α
(
σ
)
|
σ

X
}⊆
Y

bydef.
α

⇐⇒∀
σ

X
:
α
(
σ
)

Y
⇐⇒
X
⊆{
σ
|
α
(
σ
)

Y
}

bydef.

⇐⇒
X

γ

(
Y
)

bydef.
γ

So
α

(
X
)

Y
ifandonlyif
X

γ

(
Y
)
,whichisacharacteristic

property
of
Galoisconnec

tions
.Galois

connections
preservejoin

s
inthat
α

(
i


X
i
)
=
{
α
(
σ
)
|
σ

i


X
i
}
=
i


{
α
(
σ
)
|
σ

X
i
}
=
i


α

(
X
i
)
.Equiv-
alentformalizationsinvolveMoorefamilies,closureoperators,etc[Cousot,
1978;CousotandCousot,1979].
8.There

exivetransitiveclosuresemanticsin

xpoint
mrofSincetheconcrete(partialtrace)semanticscanbeexpressedin

xpointform
andtheabstract(re

exivetransitiveclosure)semanticsisanabstractionofthe
concretesemanticsbyaGaloisconnection,wecanalsoexpresstheabstract
semanticsin

xpointform.ThisisageneralprincipleinAbstractInterpretation
[CousotandCousot,1979].
Wehave
∅⊆
γ

(

)
whence
α

(

)
⊆∅
proving
α

(

)=

byantisymmetry.
Forallsets
X
ofpartialtraces,wehavethe
commutationproperty
:
α

(
F
τ

(
X
))
=
α

(
{
s
|
s

Σ
}∪{
σss

|
σs

X

s,s


t
}
)

def.
F
τ

=
{
α
(
s
)
|
s

Σ
}∪{
α
(
σss

)
|
σs

X

s,s


t
}
)

def.
α

=
{
s,s
|
s

Σ
}∪{
σ
0
,s

|∃
s
:
σs

X

s,s


t
}
)

def.
α
=
1
Σ
∪{
σ
0
,s

|∃
s
:

σ
0
,s

α

(
X
)

s,s


t
}
)

def.
1
S
=
{
x,x
|
x

S
}
and
α

=
1
Σ

α

(
X
)

t

def.composition

ofrelations
=
F
τ

(
α

(
X
))

byde

ning
F
τ

(
Y
)
=
1
Σ

Y

t

nIffollows,byrecurrence,thattheiterates
F
τ

(

)
of
F
τ

andthose
F
τ

n
(

)
of
F
τ

arerelatedby
α

.Forthebasis,
α

(
F
τ

0
(

))
=

=
F
τ

0
(

)
.Forthein-
n1+nnductionstep,if
α

(
F
τ

(

))
=
F
τ

n
(

)
then
α

(
F
τ

(

))
=
α

(
F
τ

(
F
τ

(

)))
n=
F
τ

(
α

(
F
τ

(

)))
=
F
τ

(
F
τ

n
(

))
=
F
τ

n
+1
(

)
.Itfollowsthat
α


τ

)
=
α

(lfp

F
τ

())
=
α

(
n

0
F
τ

n
(

))
=
n

0
α

(
F
τ

n
(

))
=
n

0
F
τ

n
(

)
=


∀⇒⇐PatrickCousot&RadhiaCousot
5
lfp

F
τ

.Thiscanbeeasilygeneralizedtoordertheory[Cousot,1978;Cousot
∅andCousot,1979]andisknownasthe

xpointtransfer
theorem.
Observethatif
Σ
is

nitethenthe

xpointde

nitionprovidesaniterative
algorithmforcomputingthere

exivetransitiveclosureofarelationas
X
0
=

,
...
,
X
i
+1
=
F
τ

(
X
i
)
,
...
,until
X
n
+1
=
X
n
=lfp

F
τ

=
t

.
∅9.Thereachabilitysemanticsasanabstractionofthe
re

exivetransitiveclosuresemantics
Thereachabilitysemanticsofthetransitionsystem
τ
=

Σ
,
Σ
i
,t

istheset
{
s

|∃
s

Σ
i
:

s,s


t

}
ofstateswhicharereachablefromtheinitialstates
Σ
i
.Thisisanabstraction
α

(
t

)
ofthere

exivetranstiveclosuresemantics
t

byde

ningtheright-image
post[
r
]
Z
=
{
s

|∃
s

Z
:

s,s


r
}
oftheset
Z
bytherelation
r
and
α

(
Y
)=post[
Y

i
=
{
s

|∃
s

Σ
i
:

s,s


Y
}
.
Let
γ

(
Z
)=
{
s,s

|
s

Σ
i
=

s


Z
}
.WehavetheGaloisconnection:
α

(
Y
)

Z
⇐⇒{
s

|∃
s

Σ
i
:

s,s


Y
}⊆
Z

def.
α


s

:

s

Σ
i
:

s,s


Y
=

s


Z

def.inclusion


s,s


Y
:
s

Σ
i
=

s


Z
}

def.implication
=

Y
⊆{
s,s

|
s

Σ
i
=

s


Z
}⇐⇒
Y

γ

(
Z
)

def.

,
γ

.

10.Thereachabilitysemanticsin

xpointform
Toestablishthecommutationproperty,weprovethat
α

(
F
τ

(
Y
))
=
{
s

|∃
s

Σ
i
:

s,s


(
1
Σ

Y

t
)
}

bydef.
α

&
F
τ

=
{
s

|∃
s

Σ
i
:
s

=
s
}∪{
s

|∃
s

Σ
i
:

s

:

s,s


Y

s

,s


t
)
}

bydef.
1
Σ
&functioncomposition

=
Σ
i
∪{
s

|∃
s


α

(
Y
)

s

,s


t
)
}

bydef.
α

=
F
τ

(
α

(
Y
))

byde

ning
F
τ

(
Z
)
=
Σ
i

post[
t
]
Z
.

⊆Bythe

xpointtransfertheorem,itfollowsthat
α

(
t

)
=
α

(lfp

F
τ

)
=
⊆lfp

F
τ

.
Observethat

if
Σ
is


nite,wehaveaforwardreachabilityiterativealgo-
rithm(since
lfp

F
τ

=
n

0
F
τ

n
(

)
)whichcanbeusedtochecke.g.that
allreachablestatessatisfyagivensafetyspeci

cation
S
:
α

(
t

)

S
n
:
F
τ

n
(

)

S
.

⇒⇐⇒⇐⇒⇐
⇒⇐⇒⇐≤⊆6
BasicConceptsofAbstractInterpretation
11.Theintervalsemanticsasanabstractionofthe
reachabilitysemantics
Incasethesetofstatesofatransitionsystem
τ
=

Σ
,
Σ
i
,t

istotallyordered

Σ
,<

withextrema
−∞
and
+

1
,theintervalsemantics
α

(
α

(
t

))
of
τ
providesboundsonitsreachablestates
α

(
t

)
:
α

(
Z
)=[min
Z,
max
Z
]
where
min
Z
(
max
Z
)isthein

mum(resp.supremum)oftheset
Z
and
min

=
+

(resp.
max

=
−∞
).Allemptyintervals
[
,h
]
with
h<
areidenti

ed
to
[+

,
−∞
]
.Byde

ningtheconcretization
γ

([
,h
])=
{
s

Σ
|

s

h
}
,wecande

netheabstractimplication
[
,h
]

[


,h

]
as
γ

([
,h
])
γ

([


,h

])
orequivalently
(





h

h

)
.WehaveaGaloisconnection:
α

(
Z
)

[
,h
]
⇐⇒
[min
Z,
max
Z
]

[
,h
]

def.
α



min
Z

max
Z

h

def.

Z
⊆{
s

Σ
|


s

h
}

def.
min
&
max
Z

γ

([
,h
])

def.
γ

Byde

ning
i


[

i
,h
i
]
=
[min
i



i
,
max
i


h
i
]
,thecharacteri

sticprop-
e

rtythatGaloisconnectionspreservesleastupperboundsisnow
α

(
i


Z
i
)=
i


α

(
Z
i
)
.
12.Theintervalsemanticsin

xpointform
Obviously,
α

(

)=[+

,
−∞
]
.Moreover:
α

(
F
τ

(
Z
))=
α


i

post[
t
]
Z
)

def.
F
τ


=
α


i
)

α

(post[
t
]
Z
)

Galoisconnection
[minΣ
i
,
maxΣ
i
]

α

(post[
t
](
γ

(
α

(
Z
))))

def.
α

andsince
Z

γ

(
α

(
Z
))
so
post[
t
]
Z

post[
t
](
γ

(
α

(
Z
)))
whence
α

(post[
t
]
Z
)

α

(post[
t
](
γ

(
α

(
Z
))))

F
τ

(
α

(
Z
))

byde

ning
F
τ

suchthat
[minΣ
i
,
maxΣ
i
]

α


post[
t
]

γ

(
I
)
F
τ

(
I
)

Weonlyhave
semi-commutation
α

(
F
τ

(
Z
))
F
τ

(
α

(
Z
))
hencea

x-
pointapproximation
[CousotandCousot,1979]:
α

(
α

(
t

))
=
α

(lfp

F
τ

)



•∗



lfp
[+

,
−∞
]
F
τ
.Soquestions
α
(
t
)

γ
(
S
)
havesoundanswers
lfp
[+

,
−∞
]
F
τ

S
intheabstract.

⇐⇒1
or,moregenerally,formacompletelattice.


PatrickCousot&RadhiaCousot
7
13.Convergenceacceleration
Ingeneral,theiterates
lfp
[+

,
−∞
]
F
τ

=
n

0
F
τ

n
([+

,
−∞
])
diverge.
Forexampleforthetransitionsystem

Z
,
{
0
}
,
{
x,x

|
x

=
x
+1
}
ofprogram
x:=0;whiletruedox:=x+1
,weget
F
τ

([
,h
])=
[0
,
0]

[

+1
,h
+1]
withdivergingiterates
[+

,
−∞
]
,
[0
,
0]
,
[0
,
1]
,
...
,
[0
,n
]
,
...
whichleastupperboundis
[0
,
+

]
.
14.Widening
Therefore,toaccelerateconvergenc

e,weintrodu

cea
widening
[Cousot
andCousot,1977]suchthat
I

IJ
,
J

IJ
andthe
iterateswith
widening
de


nedas
I
0
=[+

,
−∞
]
,
I
n
+1
=
I
n
if
F
τ

(
I
n
)

I
n
while
I
n
+1
=
I
n
F
τ

(
I
n
)
otherwisedoconverge.Thentheirlimit
I
λ
is

nite
(
λ

N
)andisa

xpointoverapproximation
lfp
[+

,
−∞
]
F
τ


I
λ
.
Anexampleofintervalwideningconsistsinchoos

inga

niteramp
−∞
=
r
0
<r
1
<...<

r
k
=+

,
k

1
and
[+

,
−∞
][


,h

]=[


,h

]
while,
otherwise,
[
,h
][


,h

]=[if


<
thenmax
{
r
i
|
r
i



}
else
,
if
h

>
h
thenmin
{
r
i
|
h


r
i
}
else
h
]
.
Forthetransitionsystem

Z
,
{
0
}
,
{
x,x

|
x<
100

x

=
x
+1
}
ofpro-
gram
x:=0;whilex<100dox:=x+1
andramp
−∞
<

1
<
0
<
1
<
+

,wehave
F
τ

([
,h
])=[0
,
0]

[

+

1
,
min(99
,h
)+1]
and
theiterateswithwidening
I
0
=

[+

,
−∞
]
,
I
1

=
I
0
F
τ

(
I
0
)=
F
τ

(
I
0
)=
[0
,
0]

[1
,
1]=[0
,
1]
,
I
2
=
I
1
F
τ

(
I
1
)=[0
,
1][0
,
2]=[0
,
+

]
.Thisisthe
limitoftheseiterateswithwideningsince
F
τ

([0
,
+

])=[0
,
100]

[0
,
+

]
.
15.Narrowing
Thelimitofaniterationwithwideningcanbeimprovedbya
narrowing
[CousotandCousot,1977]suchthat
J

I
implies
J

IJ

I
.Allterms
inthe
iterateswithnarrowing
J
0
=
I
λ
,
...
,
J
n
+1
=
J
n
F
τ

(
J
0
)
improve
theresultobtainedbywideningsince
lfp
[+

,
−∞
]
F
τ


J
n

I
λ
.
Anexampleofintervalnarrowingis
[
,h
]

[


,h

]=[if

i
:

=
r
i
then


else
,
if

j
:
h
=
r
j
then
h

else
h
]
.
Fortheprogram
x:=0;whilex<100dox:=x+1
,wehave
J
0
=
[0
,
+

]
,
J
1
=
[0
,
+

]

F
τ

([0
,
+

])
=
[0
,
+

]

[0
,
100]
=
[0
,
100]
and
so
J
n
=
[0
,
100]
for
n

1
since
F
τ

([0
,
100])=[0
,
100]
.
16.Compositionofabstractions
Wehavede

nedthreeabstractionsofthepartialtracesemantics
Σ
τ

ofa
transitionsystem
τ
.Thedesignwascompositionalinthatthecomposition

8
BasicConceptsofAbstractInterpretation

α


α
•◦
α


∗◦
γ
•◦
γ


ofGaloisconnectionsisaGaloisconnectionso
thesuccessiveargumentsonsoundapproximationsdocomposenicely.
17.Hierarchyofsemantics
Thefoursemanticsofatransitionsystem
τ
=

Σ
,
Σ
i
,t

thatwehavecon-
sideredformahierarchyfromthepartialtraces
Σ
τ

,tothere

exivetransitive
closure
α


τ

)
,reachability
α
•◦
α


τ

)
andintervalsemantics
α


α
•◦
α


τ

)
,inabstractionorder.Thecompleterangeofotherpossibleabstractse-
manticsincludeallclassicalonesforprogramminglanguages[Cousot,2002].
Byundecidability,noneiscomputable,buteffectivewidening/narrowingiter-
ationscanbeusedtocomputeapproximations(whicharemoreprecisethan
resortingto

niteabstractions,asinabstractmodelchecking[Cousotand
Cousot,1992b]).Moreabstractsemanticscananswerlessquestionsprecisely
thanmoreconcretesemanticsbutarecheapertocomputeorapproximate.
Thiscoversallstaticanalysis,includingdata

owanalysis[CousotandCousot,
1979],abstractmodelchecking[Cousot,2000b],typing[Cousot,1997],etc.
Inpracticetherightbalancebetweenprecisionandcostcanleadtopreciseand
ef

cientabstractions,asforexamplein
Astrée
[Blanchetetal.,2003].
References
Blanchet,B.,Cousot,P.,Cousot,R.,Feret,J.,Mauborgne,L.,Miné,A.,Monniaux,D.,and
Rival,X.(2003).Astaticanalyzerforlargesafety-criticalsoftware.
PLDI’2003
,196–207,
.MCACousot,P.(1978).Méthodesitérativesdeconstructionetd’approximationdepoints

xesd’opé-
rateursmonotonessuruntreillis,analysesémantiquedeprogrammes.Thèsed’Étatèsscie-
ncesmathématiques,GrenobleUniversity,21March1978.
Cousot,P.(1981).Semanticfoundationsofprogramanalysis.InMuchnick,S.S.andJones,
N.D.,editors,
ProgramFlowAnalysis:TheoryandApplications
,ch.10,303–342.Prentice-
.llaHCousot,P.(1997).Typesasabstractinterpretations.
24thPOPL
,316–331,ACM.
Cousot,P.(2000a).Abstractinterpretationbasedformalmethodsandfuturechallenges.
«In-
formatics—10YearsBack,10YearsAhead»
,LNCS2000,138–156,Springer.
Cousot,P.(2000b).Partialcompletenessofabstract

xpointchecking.
SARA’2000
,LNAI1864,
1–25,Springer.
Cousot,P.(2002).Constructivedesignofahierarchyofsemanticsofatransitionsystemby
abstractinterpretation.
Theoret.Comput.Sci.
,277(1—2):47–103.
Cousot,P.andCousot,R.(1977).Abstractinterpretation:auni

edlatticemodelforstaticanaly-
sisofprogramsbyconstructionorapproximationof

xpoints.
4thPOPL
,238–252,ACM.
Cousot,P.andCousot,R.(1979).Systematicdesignofprogramanalysisframeworks.
6th
POPL
,269–282,ACM.
Cousot,P.andCousot,R.(1992a).Abstractinterpretationframeworks.
J.LogicandComp.
,
2(4):511–547.
Cousot,P.andCousot,R.(1992b).ComparingtheGaloisconnectionandwidening/narrowing
approachestoabstractinterpretation.
PLILP’92
,LNCS631,269–295,Springer.