summaryrefslogtreecommitdiffstats
path: root/doc/soutenance/soutenance.tex
blob: 905a6b6a772343f6d506f42f4e3267aa69246a96 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456

\nonstopmode

\documentclass{beamer}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{hhline}
\usepackage{caption}
\usepackage[notocbib]{apacite}
\usetheme{Luebeck}
\useoutertheme[footline=authortitle,subsection=false]{miniframes}

\usepackage{tikz}
\usetikzlibrary{positioning}
\usetikzlibrary{trees}
\tikzstyle{level 1}=[level distance=2cm, sibling distance=5.2cm]
\tikzstyle{level 2}=[level distance=1.7cm, sibling distance=2.6cm]
\tikzstyle{var}=[circle, draw=black, thick, text centered]
\tikzstyle{end}=[draw=black, thick, text centered]

\usepackage{tabularx}
\newcolumntype{b}{X}
\newcolumntype{s}{>{\hsize=.5\hsize}X}
\newcolumntype{t}{>{\hsize=.3\hsize}X}
\newcolumntype{u}{>{\hsize=.1\hsize}X}
\newcommand{\heading}[1]{\multicolumn{1}{|c}{#1}}
\newcommand{\llrrbracket}[1]{% \llrrbracket{..}
  \left[\mkern-3mu\left[#1\right]\mkern-3mu\right]}

\usepackage{multicol}

% -----------------------
% entete

\title{Analyse statique de SCADE par interprétation abstraite}
\author{Alex AUVOLAT}
\date{Juillet 2014}

\begin{document}

\begin{frame}
\titlepage
\end{frame}

\begin{frame}\frametitle{Introduction}
  \begin{itemize}
    \item On cherche à vérifier des propriétés sur des programmes SCADE (propriétés générales ou propriétés spécifiées dans le code)
    \item Différentes techniques d'analyse existent~: interprétation abstraite (Astrée), model checking (DV, Kind, GATeL)
    \item Motivation~: en faisant l'analyse directement sur SCADE, on se passe d'un certain nombre de problèmes spécifiques à C (modèle mémoire, initialisation, ...)
  \end{itemize}
\end{frame}

\begin{frame}
\frametitle{Plan}
\tableofcontents
\end{frame}

% ----------------------
% contenu

\section{Généralités sur SCADE}
\frame{\sectionpage}
\begin{frame}\frametitle{Environnements mémoire}
  Soit un programme SCADE, on note~:
  \begin{itemize}
    \item  $\mathbb{X}$ l'ensemble de ses variables ;
    \item $\mathbb{V}$ l'ensemble des valeurs qu'elles peuvent prendre.
  \end{itemize}
  \begin{definition}
    Un envrionnement mémoire est une fonction de $\mathbb{X}\to\mathbb{V} = \mathbb{M}$
  \end{definition}
  Dans notre étude, on est ammené à étudier des ensembles d'environnements mémoire, c'est-à-dire des éléments de $\mathcal{P}(\mathbb{M})$.

  On bénéficie de la structure de treillis de $(\mathcal{P}(\mathbb{M}), \emptyset, \mathbb{M}, \subseteq, \cup, \cap)$.
\end{frame}
\begin{frame}\frametitle{Système de transition, fonction de transition}
  Un programme SCADE représente une fonction de transition~:
  $$s_0 \xrightarrow{i_1} s_1 \xrightarrow{i_2} s_2 \xrightarrow{i_3} \cdots$$
  On peut réécrire cette sémantique de transition avec deux fonctions: $c$, qui copie une partie de $s_{n-1}$ dans $s_n$ pour garder des mémoires, et $f$ qui prend ces mémoires ainsi que les entrées pour calculer $s_n$:
  $$s_n = f(c(s_{n-1}) + i_n)$$
\end{frame}
\begin{frame}\frametitle{Sémantique collectrice}
  On s'intéresse aux états du programme pour toutes les entrées possibles~:
  $$g(A) = \{ f(c(s) + i), s \in A, i \in \mathbb{I} \}$$
  Puis on s'intéresse à tous les états du programme, à tous les cycles~:
  $$S = lfp_{S_0} ( \lambda A. A \cup g(A) )$$
  $$S \in \mathcal{P}(\mathbb{M})$$
  Où $S_0$ est l'ensemble des états mémoire initiaux pour le programme.
\end{frame}
\begin{frame}\frametitle{Preuve de propriétés}
  La sémantique collectrice $S$ représente une première abstraction de notre programme~: c'est l'ensemble de tous les états mémoire accessible par notre programme, quelque soient les entrées, et à tout moment de l'exécution.

  Prouver une propriété $P$, c'est montrer que $\forall s \in S, P(S)$.
\end{frame}
\section{Interprétation abstraite}
\frame{\sectionpage}
\begin{frame}\frametitle{Abstraction}
  Pour pouvoir travailler sur $\mathcal{P}(\mathbb{M})$ de manière algorithmique, c'est-à-dire faire une analyse qui termine, on procède par abstraction.
  
  Pour cela on représente les valeurs dans un domaine abstrait $\mathcal{D}^\sharp$.
  \begin{definition}
    Fonctions d'abstraction et de concretisation~:
    $$\alpha: \mathcal{P}(\mathbb{M}) \to \mathcal{D}^\sharp$$
    $$\gamma: \mathcal{D}^\sharp \to \mathcal{P}(\mathbb{M})$$
  \end{definition}
  Pour représenter $s \in \mathcal{P}(\mathbb{M})$, on utilise toujours une valeur abstraite $s^\sharp$ {\em sûre}, c'est-à-dire que $s \subset \gamma(s^\sharp)$.
\end{frame}
\begin{frame}\frametitle{Abstraction}
  \begin{figure}
    \centering
    \def\svgwidth{.9\textwidth}
    \input{alpha-gamma.pdf_tex}
  \end{figure}
\end{frame}
\begin{frame}\frametitle{Structure de treillis}
  On définit deux valeurs abstraites particulières~:
  \begin{itemize}
    \item $\bot$~: $\gamma(\bot) = \emptyset$
    \item $\top$~: $\gamma(\top) = \mathbb{M}$
  \end{itemize}
  On définit également des opérateurs sur nos valeurs abstraites~:
  \begin{itemize}
    \item $\sqcup$~: $\gamma(s) \cup \gamma(s') \subset \gamma(s \sqcup s')$
    \item $\sqcap$~: $\gamma(s) \cap \gamma(s') \subset \gamma(s \sqcap s')$
  \end{itemize}
  Ce qui munit $\mathcal{D}^\sharp$ d'une structure de treillis~: $(\mathcal{D}^\sharp, \bot, \top, \sqsubseteq, \sqcup, \sqcap)$.

  On cherche à chaque fois à trouver une meilleure approximation possible de $\gamma(s) \cup \gamma(s')$ ou $\gamma(s) \cap \gamma(s')$, sans jamais rien perdre (propriété de sûreté).
\end{frame}
\begin{frame}\frametitle{Abstraction non relationnelle}
    On peut utiliser une abstraction qui traîte chaque variable séparément, en indiquant dans quel intervalle de valeurs elle évolue~:
    $$\mathcal{D}^\sharp = \mathbb{X} \to itv(\mathbb{Z})$$
    ($itv(\mathbb{Z})$ est lui-même muni d'une structure de treillis)
  \begin{example}
    Par exemple si on a rencontré les environnements $\{x=0, y=5\}$ et $\{x=1, y=4\}$, on peut les représenter par la valeur abstraite $s$ telle que~:
    $$s(x) = [0, 1]$$
    $$s(y) = [4, 5]$$
  \end{example}
\end{frame}
\begin{frame}\frametitle{Abstraction relationnelle}
  On peut utiliser une abstraction qui mémorise des relations entre les variables. La plus célèbre est l'ensemble des polyèdres convexes, qui représente un ensemble d'environnements comme une conjonction d'égalités ou d'inégalités linéaires sur les variables.
  \begin{example}
    Par exemple si on a rencontré les environnements $\{x=0, y=5\}$ et $\{x=1, y=4\}$, on peut les représenter par la valeur abstraite $s$ qui contient les contraintes suivantes~:
    $$0 \le x \le 1$$
    $$y = 5 - x$$
  \end{example}
\end{frame}
\begin{frame}\frametitle{Opérateur de widening}
  L'opérateur de widening, habituellement noté $\nabla$, est un opérateur crucial pour faire terminer l'analyse des boucles.

  Pour les intervalles, il s'agit généralement d'envoyer une borne à l'infini~:
  $$[1,3] \nabla [1,4] = [1, \infty]$$
  Pour les polyèdres, c'est plus complexe mais globalement cela peut se comprendre comme la suppression d'une ou de plusieurs contraintes.

  \begin{example}
    Par exemple si on étudie un compteur qui est incrémenté à chaque tour de boucle, on va rencontrer les valeurs $x=1$, $x=2$, $x=3$, ...
    
    L'opérateur $\nabla$ permet d'extrapoler pour pouvoir dire~: $x$ varie dans $\mathbb{N}^*$.
  \end{example}
\end{frame}

\begin{frame}\frametitle{Abstraction de la sémantique collectrice, preuve de propriétés}
  Si on souhaite prouver par exemple qu'une variable booléenne $p$ est toujours vraie, alors on a besoin de montrer que~:
  $$\forall s \in S, s(p)=true$$

  On ne peut pas manipuler $S$ directement, mais on peut en manipuler une abstraction $S^\sharp$ telle que $S \subset \gamma(S^\sharp)$.

  $S^\sharp$ est également défini comme un point fixe~:
  $$S^\sharp = lfp_{S_0^\sharp} (\lambda s. s^\sharp \sqcup g^\sharp(s))$$
  
  Si on montre que $p=true$ dans $S^\sharp$, c'est gagné.
\end{frame}
\begin{frame}\frametitle{Preuve de propriété}
  \begin{figure}
    \centering
    \def\svgwidth{.75\textwidth}
    \input{property.pdf_tex}
  \end{figure}
\end{frame}

\section{Domaines à disjonction de cas}
\frame{\sectionpage}
\begin{frame}\frametitle{Besoin d'une abstraction performante}
  \begin{itemize}
    \item On veut être capable de traîter correctement l'initialisation
    \item On veut être capable d'étudier les états d'automates ou les branches de conditions séparément
    \item On veut être capable d'utiliser des variables booléennes pour partitionner notre représentation abstraite
  \end{itemize}
  Les domaines relationnels à base de polyèdres ou d'octogones ne sont pas à même de représenter des contraintes qui mettent en relation des variables énumérées et des variables numériques.

  Il a donc fallu développer de nouveaux domaines abstraits mieux adaptés.
\end{frame}
\begin{frame}[fragile]\frametitle{Un exemple}
  Étudions un programme simple~:
  \vspace{7mm}

  \begin{verbatim}
    lx = 0 -> pre x
    c = (lx >= 10)
    x = if c then 0 else lx + 1
  \end{verbatim}
  \vspace{7mm}

  On aimerait prouver $x \in [0,10]$
\end{frame}
\begin{frame}\frametitle{Itérations sur cet exemple}
  Dans le cas où l'on ne fait pas de disjonctions, nos itérations vont ressembler à ça~:
  \vspace{5mm}

  \begin{tabularx}{\linewidth}{|s|b|b|b|b|}
    \hhline{-----}  iter & \begin{bf}init\end{bf} & $\mathbf{lx}$ & $\mathbf{c}$ & $\mathbf{x}$ \\
    \hhline{|=|=|=|=|=|}
      0 &       tt & 0 & ff & 1 \\ \hhline{-----}
      1 &       $\top$ & $[0,1]$ & ff & $[1,2]$ \\ \hhline{-----}
      2 &       $\top$ & $[0,2]$ & ff & $[1,3]$ \\ \hhline{-----}
      3 &       $\top$ & $[0,3]$ & ff & $[1,4]$ \\ \hhline{-----}
      4 &       $\top$ & $[0,\infty[$ & $\top$ & $[0,\infty[$ \\ \hhline{-----}
      5 &       $\top$ & $[0,\infty[$ & $\top$ & $[0,\infty[$ \\ \hhline{-----}
  \end{tabularx}
  \vspace{5mm}

  On n'a pas réussi à prouver une borne supérieure sur $x$ !
\end{frame}
\begin{frame}\frametitle{Disjonctions de cas selon des variables}
  On se done un ensemble $\mathbb{X}_d$ de variables énumérées (prenant leurs valeurs dans $\mathbb{V}_d$ un ensemble fini).
  
  On note $\mathbb{M}_d = \mathbb{X}_d \to \mathbb{V}_d$.
  \begin{definition}
    On définit le domaine abstrait suivant~:
    $$\mathcal{D}^\sharp_d = \mathbb{M}_d \to \mathcal{D}^\sharp$$
  \end{definition}
  Chaque combinaison possible pour les variables de $\mathbb{V}_d$ est traîtée séparément. En pratique tous les cas ne sont pas toujours accessibles.
\end{frame}
\begin{frame}\frametitle{Exemple}
  Une représentation appropriée pour traiter notre exemple serait~:
  \vspace{5mm}

  \begin{tabularx}{\linewidth}{|s|s|b|}
    \hline  \begin{bf}init\end{bf} & $\mathbf{c}$ & \\
    \hhline{|=|=|=|}
      tt & tt & $\bot$ \\ \hline
      tt & ff & $lx = 0; x = 1$ \\ \hline
      ff & tt & $lx = 10; x = 0$ \\ \hline
      ff & ff & $0 \le lx \le 9; x = lx + 1$ \\ \hline
  \end{tabularx}
    
\end{frame}
\begin{frame}\frametitle{Opérateurs correspondants}
  La fonction de concrétisation donne la sémantique du domaine~:
  $$\forall s \in \mathcal{D}_d^\sharp, \gamma(s) = \bigcup_{d\in\mathbb{M}_d} \left\{ e \in \gamma(s(d)) \;|\; \forall x \in \mathbb{X}_d, e(x)=d(x) \right\}$$

  Si on considère une contrainte sur des variables énumérées du type $x \equiv y$, on est capable de la traîter comme suit~:
  $$\llrrbracket{ x \equiv y}(s)
    =  \lambda d.
        \begin{cases} s(d) & \text{si } d(x) = d(y)
                    \\ \bot & \text{sinon}
        \end{cases}$$
  Les opérateurs $\sqcap, \sqcup$ et les valeurs $\top, \bot$ ne posent pas de problème. Par exemple, $s \sqcup s' = \lambda d. s(d) \sqcup s'(d)$.
\end{frame}
\begin{frame}\frametitle{Principe d'itération}
  On pourait faire des itérations globales sur notre environnement de $\mathcal{D}_d^\sharp$ jusqu'à trouver un point fixe, mais pour accélerer l'analyse et pour en améliorer la précision, on considère les cas un par un.
  \begin{itemize}
    \item Prendre un cas nouveau
    \item Rechercher un point fixe pour ce cas-là ; on profite alors des conditions qui font que l'on reste dans ce cas d'un cycle au suivant, à la manière de conditions de sortie de boucle, pour affiner l'analyse
    \item Effectuer un cycle complet sans restriction, en partant de ce point fixe, et considérer tous les nouveaux cas que l'on a découvert
  \end{itemize}
  C'est le principe des {\em itérations chaotiques}.
\end{frame}
\begin{frame}\frametitle{Itérations chaotiques sur notre exemple}
  Reprenons notre exemple. Maintenant, on a~:

  \begin{tabularx}{\linewidth}{|su|b|b|b|b|}
    \hhline{------}  & & \begin{bf}init\end{bf} & $\mathbf{lx}$ & $\mathbf{c}$ & $\mathbf{x}$ \\
    \hhline{|==|=|=|=|=|}
      0 & $\star$ &  tt & 0 & ff & 1 \\ \hhline{------}
      1 &         &  $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
        & $\star$ &  $ff$ & $1$ & ff & $2$ \\ \hhline{------}
      2 &         &  $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
        &         &  $ff$ & $[1,9]$ & ff & $[2,10]$ \\ \hhline{|~~|----}
        & $\star$ &  $ff$ & $10$ & tt & 0  \\ \hhline{------}
      3 &         &  $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
        & $\star$ &  $ff$ & $[0,9]$ & ff & $[1,10]$ \\ \hhline{|~~|----}
        &         &  $ff$ & $10$ & tt & 0 \\ \hhline{------}
      4 &         &  $tt$ & $0$ & ff & $1$ \\ \hhline{|~~|----}
        &         &  $ff$ & $[0,9]$ & ff & $[1,10]$ \\ \hhline{|~~|----}
        &         &  $ff$ & $10$ & tt & 0 \\ \hhline{------}
  \end{tabularx}
\end{frame}
\begin{frame}\frametitle{Problème d'explosion}
  On peut avoir à représenter des valeurs abstraites comme la suivante~:
  \vspace{5mm}

  \begin{tabularx}{\linewidth}{|t|t|t|b|}
    \hhline{----}  \begin{bf}init\end{bf} & $\mathbf{la}$ & $\mathbf{lb}$ & \\
    \hhline{|=|=|=|=|}
      tt & tt & tt & $a = 0; b = 0$ \\ \hhline{----}
      tt & tt & ff & $a = 0; b = 0$ \\ \hhline{----}
      tt & ff & tt & $a = 0; b = 0$ \\ \hhline{----}
      tt & ff & ff & $a = 0; b = 0$ \\ \hhline{----}
      ff & tt & tt & $a = 0; b \in [1, \infty[$ \\ \hhline{----}
      ff & tt & ff & $a = 1; b \in [1, \infty[$ \\ \hhline{----}
      ff & ff & tt & $a = -1; b \in [1, \infty[$ \\ \hhline{----}
      ff & ff & ff & $a = 0; b \in [1, \infty[$ \\ \hhline{----}
  \end{tabularx}
  \vspace{5mm}

  Il y a beaucoup de redondance !
\end{frame}
\begin{frame}\frametitle{La solution}

  \begin{figure}\centering
    \begin{tikzpicture}[->]
      \node[var, text centered] (init) {init};
      \node[var, below right = .7cm and 1.5cm of init] (la) {la};
      \node[var, below left = .7cm and .4cm of la] (lb1) {lb};
      \node[var, below right = .7cm and .4cm of la] (lb2) {lb};
      \node[end, below left = 1cm and .4cm of lb1] (f2) {$\begin{tabular}{c}a = -1\\b \in [1,\infty[\end{tabular}$};
      \node[end, right = .5cm of f2] (f3) {$\begin{tabular}{c}a = 0\\b \in [1, \infty[\end{tabular}$};
      \node[end, below right = 1cm and .4cm of lb2] (f4) {$\begin{tabular}{c}a = 1\\b \in [1, \infty[\end{tabular}$};
      \node[end, left = .6cm of f2] (f1) {$\begin{tabular}{c}a = 0\\b = 0\end{tabular}$};

      \path[->, thick]
        (init) edge node [left] {$tt$} (f1)
               edge node [right] {$ff$} (la)
        (la) edge node[left] {$ff$} (lb1)
             edge node[right] {$tt$} (lb2)
        (lb1) edge node[left] {$tt$} (f2)
              edge node[right] {$ff$} (f3)
        (lb2) edge node[left] {$tt$} (f3)
              edge node[right] {$ff$} (f4)
    \end{tikzpicture}
  \end{figure}
\end{frame}

\begin{frame}\frametitle{Disjonctions de cas avec graphe de décision}
  On numérote les variables de $\mathbb{V}_d$~: $x_1, x_2, \dots, x_m$.

  On considère un type somme qui représente un graphe de décision~:
  $$ \begin{tabular}{rcl}
    T & := & V(s), s \in \mathcal{D}^\sharp \\
      & |  & C(x_i, v_1 \to T_1, \dots, v_k \to T_k)
    \end{tabular} $$
  La sémantique est donnée par la fonction de concrétisation~:
  $$ \begin{tabular}{rcl}
      \gamma(V(s)) & = & \gamma(s) \\
      \gamma(C(x, v_1 \to T_1, \dots, v_k \to T_k) & = &
        \bigcup_{i=1}^k \{ e \in \gamma(T_i) \;|\; e(x) = v_i \}
    \end{tabular} $$
  On impose que si un noeud $C(x_i, \dots)$ est parent d'un noeud $C(x_j, \dots)$, alors $i < j$, ce qui implique l'unicité de l'arbre.
\end{frame}
\begin{frame}[fragile]\frametitle{Retour à notre exemple}
  Notre exemple peut être représenté par la structure suivante~:
  \begin{figure}\centering
    \begin{tikzpicture}[->,thick]
      \node[var] {init}
        child {
            node[var] {c}
              child {
                node[end] {$\bot$}
                  edge from parent
                  node[left]{tt}
              }
              child {
                node[end] {$\begin{tabular}{c}lx = 0 \\ x = 1\end{tabular}$}
                  edge from parent
                  node[right]{ff}
              }
              edge from parent
              node[left] {tt}
        }
        child {
            node[var] {c}
              child {
                node[end] {$\begin{tabular}{c}lx = 10 \\ x = 0\end{tabular}$}
                  edge from parent
                  node[left]{tt}
              }
              child {
                node[end] {$\begin{tabular}{c}0 \le lx \le 9 \\ x = lx + 1\end{tabular}$}
                  edge from parent
                  node[right]{ff}
              }
              edge from parent
              node[right] {ff}
        };
    \end{tikzpicture}
  \end{figure}
\end{frame}
\begin{frame}\frametitle{Opérateurs correspondants}
  \begin{itemize}
    \item On fait du partage sur les feuilles et les sous-arbres identique, ce qui transforme notre structure en un DAG.
    \item Les opérateurs $\sqcup$ et $\sqcap$ sont implémentés par récurrence, mais il faut utiliser une procédure de mémoisation pour éviter que la complexité soit exponentielle (on profite du partage).
    \item L'application d'une condition sur les énumérés $x \equiv y$ s'effectue en faisant le $\sqcap$ avec un graphe qui représente cette contrainte.
  \end{itemize}
\end{frame}
\begin{frame}\frametitle{Principe d'itération}
  On pourait de même faire des itérations globales, mais on a préféré implémenter les itérations chaotiques pour les mêmes raisons.

  Pour identifier les différents cas, on utilise la fonction suivante, qui extrait d'un graphe la fonction booléenne sur les variables énumérées qui mène à une feuille $V(s_0)$ (partagée)~:
  $$ \begin{tabular}{rcl}
    \rho(V(s), s_0) & = & \begin{cases} \top & \text{si } s = s_0 \\ \bot & \text{sinon} \end{cases} \\
    \rho(C(x_i, v_1 \to T_1, \dots), s_0) & = & C(x_i, v_1 \to \rho(T_1, s_0), \dots)
    \end{tabular}$$
\end{frame}





\section{Résultats et conclusion}
\frame{\sectionpage}
\begin{frame}\frametitle{Comparaison avec Astrée}
  \begin{itemize}
    \item Astrée implémente un domaine abstrait permettant de traiter différents cas dans un arbre de disjonctions, mais les feuilles de cet arbre ne peuvent être que des intervalles de valeurs (ils ne gèrent pas les relations entre les variables). En conséquence, une propriété comme celle du double updown est difficile à montrer.
    \item Dans Astrée, les variables sont considérées par {\em packs}. Pour les octogones, des packs sont générés automatiquement. Pour l'arbre de disjonctions, il faut spécifier manuellement que l'on veut que l'analyseur considère un pack comportant telles et telles variables. (L'ensemble des propriétés prouvées est la conjonction des propriétés prouvées à l'aide de chaque pack).
    \item Astrée travaille sur du C, et se pose des questions inutiles (typiquement les questions d'initialisation ou de bornes)
  \end{itemize}
\end{frame}
\begin{frame}\frametitle{Implémentation}
  $\exists$ prototype.
\end{frame}
\begin{frame}\frametitle{Résultats}
  Plein de preuves sympathiques~:
  \begin{itemize}
    \item compteurs
    \item updown
    \item double updown
    \item suite de cartes
    \item un train \cite{halbwachs94c}
    \item un demi-tour pour des rames de metro \cite{lesartse}
  \end{itemize}
\end{frame}
\begin{frame}\frametitle{Limitations}
  \begin{itemize}
    \item Pour certains problèmes, il faut rajouter manuellement des variables booléennes pour faire des disjonctions de cas
    \item On ne sait pas comment ça se comporte sur des gros programmes
    \item Aucune analyse des propriétés des nombres flottants
    \item Analyseur non vérifié~: il manque quelques preuves concernant les abstractions (structures de treillis, connection de Galois, correction et terminaison des principes d'itérations chaotiques)
  \end{itemize}
\end{frame}
\begin{frame}\frametitle{Perspectives}
  \begin{itemize}
    \item Développement d'une heuristique qui détermine quelles variables représentent la structure de contrôle du programme et sont pertinentes à considérer
    \item Partitionnement dynamique
    \item Analyses par packs de variables, comme Astrée
  \end{itemize}
\end{frame}
\begin{frame}\frametitle{Références}
  \bibliographystyle{apacite}
  \bibliography{research}
\end{frame}


\end{document}