APPROCHE THEMATIQUE DU VIEILLISSEMENT

Antoine Mine

Description

DEUXIEME PARTIE APPROCHE THEMATIQUE DU VIEILLISSEMENT Rapport final – Vieillissement démographique et territoires en Nord-Pas de Calais à l'horizon 2025 1

• cadre de vie hors travail


• métropole lille


• références dans la doctrine sociale de l'eglise


• société industrielle


• régional


• population ouvrière urbaine


• cultures urbaines


• pratique sociale


• action politique

Sujets

• Kingdom of the Netherlands
• Toulouse
• Bruay-sur-l'Escaut
• Société industrielle
• Regional
• Cultures urbaines

Informations

• Publié par: profil-urra-2012
• Nombre de lectures: 20

Extrait

February3acirsbAl2102emuNnsaitoAnactromtD87

Numerical Abstract Domains MPRI 2–6: Abstract Interpretation, application to verification and static analysis

.p/1nie´niMe

´ CNRS, Ecole normale superieure ´

AntoineMine´

3 February 2012

tiucodtrIn Ou on intle AbalrastDoctinmatnAsenio´niM2.pe3Feburra2y10N2mureci

Bibliography ([exemple])

Floating-pointabstractions

Generalities, notations (reminders)

Someapplicationsof numerical domains

Handlingnon-linear expressions

Presentation of a fewnumerical abstract domains non-relational domains:intervals,congruences linear equalitydomains polyhedradomain(double description) weakly relational domains:zones,octagons

7/8

3

February

hSroctmonigsofnon-relationa

Shortcomings

2012

ldoma

of

Numerical Abstract

ins

non-relational

Domains

domains

AntoineMin´e

p.

3

/

78

rimeNu12trbslAcaeF302yraurb´ep.eMin

To prove that, e.g.Y≥ −128, we must be able to: representthe propertiesR=X−SandR≤ −D, combinethem to deduceS−X≥D, and thenY=S−D≥X.

Iterations in the interval domain (without widening): X • ]0 X • ]1 X • ]2 . . .X • ]n Y= 0|Y| ≤144|Y| ≤ . .160 .|Y| ≤128 + 16n In fact,Y∈[−128,128]always holds.

X: input signal Y: output signal S output: last R: deltaY-S D for allowed: max.|R|

4/78moiacaDtotnisnnA

Y:=0; while•true do X:=[-128,128]; D:=[0,16]; S:=Y; Y:=X; R:=X-S; if R<=-D then Y:=S-D fi; if R>=D then Y:=S+D fi done

Rate limiter

Non-relation domains cannot represent variablerelationships.

-relfnonngsocomiohtrS nrpcesioilongofssmucutila iamo cA snoitadlan

3eFrbauyr0221uNembslAcariomtDactrotnAsniae´niMeni78

To prove some invariant after theend of a loop, we often need to find aloopinvariant of amore complex form.

p.5/

To find thisioatlnanonler-invariant, we must find arelationalloop invariant at•:(−I<X<I)∧(X+I≡1 [2])∧(I∈[1,5000]), and apply the loop exit condition C ] JI>=5000K.

relational loop invariant

X:=0; I:=1; while•I<5000 do if ? then X:=X+1 else X:=X-1 fi; I:=I+1 done

A non-relational analysis finds atthatI= 5000 andX∈Z.

The best invariant is: (I= 5000)∧(X∈[−4999,4999])∧(X≡0 [2]).

letaoianendeofrr mains The tionaldo-nonalernimofosgShtcor vnipoollstnaira

3

February

2012

Numerical

Reminders

Reminders

Abstract

Domains

Antoine

Mine ´

p.

6

/

78

assignment intoV∈V test,./∈ {=, <, >, <=, >=, <>}

arithmetic expressions:

Fixed finite set of variablesV, with value inI,I∈ {Z,Q,R,M,F}

commands:

variableV∈V negation binary operation: ∈ {+,−,×, } constant range,c,c 0 ∈I∪ {±∞} cis a shorthand for [c,c]

exp::=V |−exp |expexp |[c,c 0 ]

com::=V := exp |exp./0

7/8ep.7Min´oinesAntF3beoDtcniambAlaartsum2Nicerarru01y2 Rrsdeinem xatnyS