No category

Download Pas d`erreurs fatales avec le tropical ! - Unithé ou café

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

Transcript

La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Pas d’erreurs fatales avec le tropical !
Unithé ou café
Xavier Allamigeon
INRIA Saclay – Ile-de-France et CMAP Ecole Polytechnique, équipe MAXPLUS
[email protected]
9 mars 2012
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 1/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’équipe MAXPLUS
Commune avec le CMAP de l’X, sur le platâl (aile 0 des labos)
• permanents : Stéphane Gaubert (boss), Marianne Akian, Cormac
Walsh, XA
• notre assistante : Wallis Filippi
• 1 postdoc (Sepideh Mirrahimi), 6 doctorants (Sylvie, Zheng,
Jean-Baptiste, Olivier, Pascal, et Victor)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 2/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
But de cet exposé
Vous montrer le lien entre :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 3/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
But de cet exposé
Vous montrer le lien entre :
• la vérification de programmes
1:
2:
3:
4:
5:
x := 0;
tant que x <= 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 3/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
But de cet exposé
Vous montrer le lien entre :
• la vérification de programmes
• la géométrie tropicale
1:
2:
3:
4:
5:
x := 0;
tant que x <= 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 3/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 4/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 5/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les bugs font partie de notre quotidien
Leur forme évolue avec le temps :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les bugs font partie de notre quotidien
Leur forme évolue avec le temps :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les bugs font partie de notre quotidien
En grand, à Times square :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les bugs font partie de notre quotidien
Longue tradition à la SNCF :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
On met du logiciel partout
Y compris dans des endroits critiques :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 7/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
On met du logiciel partout
Y compris dans des endroits critiques :
Ce qui mène parfois à :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 7/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes
Cela consiste à développer des outils d’analyse statique de logiciels :
• apportant l’assurance qu’il n’y a pas de bogues
• (presque) entièrement automatiques
• capables de s’attaquer à de très gros codes
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 8/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes
Cela consiste à développer des outils d’analyse statique de logiciels :
• apportant l’assurance qu’il n’y a pas de bogues
• (presque) entièrement automatiques
• capables de s’attaquer à de très gros codes
Quels genres de bugs ?
• division par zero : 1/0 retourne une erreur
• dépassement de capacité
15561676378226 ∗ 387326762373690 = −2585705764785308204
• etc
=⇒ les outils de vérification de logiciels doivent en fait s’assurer que
certaines bonnes propriétés sont satisfaites.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 8/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes (2)
Trois grands paroisses :
• l’approche par model checking (Clarke, Sifakis, Prix Turing 2007)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 9/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes (2)
Trois grands paroisses :
• l’approche par model checking (Clarke, Sifakis, Prix Turing 2007)
• par assistant de preuve, par exemple Why (PROVAL)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 9/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes (2)
Trois grands paroisses :
• l’approche par model checking (Clarke, Sifakis, Prix Turing 2007)
• par assistant de preuve, par exemple Why (PROVAL)
• par interprétation abstraite (Cousot & Cousot)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 9/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
• à la ligne 1, x vaut 0
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
• à la ligne 1, x vaut 0
• comme x est plus petit que 5, on rentre dans la boucle
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
• à la ligne 1, x vaut 0
• comme x est plus petit que 5, on rentre dans la boucle
• à la ligne 3, x vaut 2,
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
• à la ligne 1, x vaut 0
• comme x est plus petit que 5, on rentre dans la boucle
• à la ligne 3, x vaut 2, puis 4,
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
• à la ligne 1, x vaut 0
• comme x est plus petit que 5, on rentre dans la boucle
• à la ligne 3, x vaut 2, puis 4, puis 6
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
•
•
•
•
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
à la ligne 1, x vaut 0
comme x est plus petit que 5, on rentre dans la boucle
à la ligne 3, x vaut 2, puis 4, puis 6
on sort de la boucle, on saute à la ligne 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite
La sémantique d’un programme décrit l’ensemble de tous les
comportements possibles du programme.
Exemple très simple :
1:
2:
3:
4:
5:
•
•
•
•
•
x := 0;
tant que x est plus petit que 5, faire
x := x + 2;
// fin de la boucle
y := 1 / x;
à la ligne 1, x vaut 0
comme x est plus petit que 5, on rentre dans la boucle
à la ligne 3, x vaut 2, puis 4, puis 6
on sort de la boucle, on saute à la ligne 5
à la ligne 5, x vaut 6, et y vaut 1/6
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
• et pourtant on en aurait besoin pour déterminer s’il y a des bugs
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
• et pourtant on en aurait besoin pour déterminer s’il y a des bugs
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Principe de l’IA : on calcule une sur-approximation de la sémantique
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
• et pourtant on en aurait besoin pour déterminer s’il y a des bugs
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Principe de l’IA : on calcule une sur-approximation de la sémantique
• on ne peut rater aucun bug
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
La vérification de programmes par interprétation abstraite (2)
• la sémantique d’un programme n’est pas calculable en général
• et pourtant on en aurait besoin pour déterminer s’il y a des bugs
ligne 1
ligne 2
ligne 3
ligne 4
ligne 5
Principe de l’IA : on calcule une sur-approximation de la sémantique
• on ne peut rater aucun bug
• mais si on n’est pas assez précis, on peut croire qu’il y a un bug
(alors qu’en fait non) → fausse alarme !
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
6 : si y >= 3 alors
7:
x := x+1;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
• ligne 2 : x = 5, y = 0,
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
6 : si y >= 3 alors
7:
x := x+1;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
• ligne 2 : x = 5, y = 0,
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
• ligne 4 : x = 0, y = 5,
6 : si y >= 3 alors
7:
x := x+1;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
• ligne 2 : x = 5, y = 0,
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
• ligne 4 : x = 0, y = 5,
• ligne 5 : l’un des deux
cas au-dessus ! donc :
0≤x≤5
0≤y≤5
6 : si y >= 3 alors
7:
x := x+1;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
• ligne 2 : x = 5, y = 0,
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
• ligne 4 : x = 0, y = 5,
• ligne 5 : l’un des deux
cas au-dessus ! donc :
0≤x≤5
0≤y≤5
• juste après la ligne 6 :
6 : si y >= 3 alors
7:
x := x+1;
0≤x≤5
3≤y≤5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
• ligne 2 : x = 5, y = 0,
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
• ligne 4 : x = 0, y = 5,
• ligne 5 : l’un des deux
cas au-dessus ! donc :
0≤x≤5
0≤y≤5
• juste après la ligne 6 :
6 : si y >= 3 alors
7:
x := x+1;
0≤x≤5
3≤y≤5
• à la ligne 7 :
1≤x≤6
3≤y≤5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
y
ligne 4
6 : si y >= 3 alors
7:
x := x+1;
ligne 2
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
A la ligne 5 :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
0≤x≤5
0≤y≤5
y
ligne 4
6 : si y >= 3 alors
7:
x := x+1;
ligne 2
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
Juste après la ligne 6 :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
0≤x≤5
3≤y≤5
y
ligne 4
6 : si y >= 3 alors
7:
x := x+1;
ligne 2
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
Juste après la ligne 6 :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
0≤x≤5
3≤y≤5
y
ligne 4
6 : si y >= 3 alors
7:
x := x+1;
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course
Exemple de sur-approximations : les intervalles
−→ on encadre chaque variable entre deux constantes
En pratique :
A la ligne 7 :
1 : si [condition aléatoire] alors
2:
x := 5, y := 0;
3 : sinon
4:
x := 0, y := 5;
5 : // fin de la conditionnelle
1≤x≤6
3≤y≤5
y
6 : si y >= 3 alors
7:
x := x+1;
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
. . . qui offrent différents niveaux de précision
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
. . . qui offrent différents niveaux de précision
y
• intervalles
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
. . . qui offrent différents niveaux de précision
y
• intervalles
• zones
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
. . . qui offrent différents niveaux de précision
y
• intervalles
• zones
• polyèdres convexes
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’interprétation abstraite : crash course (2)
Il y a plusieurs moyens d’approximer, par exemple :
• intervals 1 ≤ x ≤ 3 (Cousot & Cousot)
• zones y − x ≥ 1 (Miné)
• polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs)
. . . qui offrent différents niveaux de précision
y
• intervalles
• zones
• polyèdres convexes
x
Problème : certaines propriétés sont difficiles à approcher
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 14/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le B.A.-BA : les algorithmes de tris
Le tri pair-impair :
5
−3
−7 −3
2
0
Blocs élémentaires :
4
1
0
2
8
4
1 −7
5
3
1
2
5
1
3
2
5
8
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 15/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le B.A.-BA : les algorithmes de tris
Le tri pair-impair :
5
−3
2
Blocs élémentaires :
4
0
8
1 −7
3
1
2
5
1
3
2
5
A la sortie,
• l’élément le plus à
gauche est le minimum
• l’élément le plus à droite
est le maximum
des éléments données en
entrée.
−7 −3
0
1
2
4
5
8
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 15/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Synthèse de plusieurs capteurs
Plusieurs capteurs pour mesurer la décélération :
L’airbag se déclenche dès qu’un des capteurs mesure une trop grande
décélération :
max(d1 , d2 , d3 ) ≥ dmax
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 16/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Synthèse de plusieurs capteurs (2)
En réalité, c’est plus compliqué −→ triplex sensor voter
(Dierkes, Cofer, Ervin, Miller, TAPAS 2010)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 17/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Synthèse de plusieurs capteurs (2)
En réalité, c’est plus compliqué −→ triplex sensor voter
(Dierkes, Cofer, Ervin, Miller, TAPAS 2010)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 17/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Synthèse de plusieurs capteurs (2)
En réalité, c’est plus compliqué −→ triplex sensor voter
Propriétés à verifier :
min(valA, valB) ≤ 0.24
min(valB, valC) ≤ 0.24
min(valA, valC) ≤ 0.24
max(valA, valB) ≥ −0.24
max(valB, valC) ≥ −0.24
max(valA, valC) ≥ −0.24
(Dierkes, Cofer, Ervin, Miller, TAPAS 2010)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 17/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Il faut manipuler la mémoire avec précaution
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Il faut manipuler la mémoire avec précaution
−→ attention aux buffer overflows
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Il faut manipuler la mémoire avec précaution
−→ attention aux buffer overflows
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Il faut manipuler la mémoire avec précaution
−→ attention aux buffer overflows
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire
C’est l’utilisation, en programmation, de
• tableaux, matrices
• chaı̂nes de caractères ("Hello World!" )
• listes, arbres, etc
=⇒ largement utilisé dans les langages de programmation moderne : C,
C++, Java, etc
Il faut manipuler la mémoire avec précaution
−→ attention aux buffer overflows
Les buffer overflows peuvent provoquer :
• un plantage de la machine (SEGFAULT)
• des trous de sécurité
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
Comment une chaı̂ne de caractères est-elle codée en machine ?
E x e m p l e \0 ? ?
longueur = 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src,
src
E x e m p l e \0 ? ?
dst
? ? ? ? ? ? ? ? ? ?
len src = 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src,
memcpy(dst, src, 9)
src
E x e m p l e \0 ? ?
len src = 7
dst
E x e m p l e \0 ? ?
len dst = 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
memcpy(dst, src, 9)
src
E x e m p l e \0 ? ?
len src = 7
dst
E x e m p l e \0 ? ?
len dst = 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
• si n ≤ len src,
src
E x e m p l e \0 ? ?
dst
? ? ? ? ? ? ? ? ? ?
len src = 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
• si n ≤ len src,
memcpy(dst, src, 5)
src
E x e m p l e \0 ? ?
len src = 7
dst
E x e m p ? ? ? ? ?
len dst ≥ 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
• si n ≤ len src, len dst ≥ n
memcpy(dst, src, 5)
src
E x e m p l e \0 ? ?
len src = 7
dst
E x e m p ? ? ? ? ?
len dst ≥ 5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
• si n ≤ len src, len dst ≥ n
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Manipulations de mémoire (2)
memcpy(dst,src,n) copie les n premiers caractères de src dans dst :
1: int i := 0;
2: for i = 0 to n-1 do
3:
dst[i] := src[i];
4: done;
• si n > len src, len dst = len src
• si n ≤ len src, len dst ≥ n
min(len dst, n) = min(len src, n)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 19/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Résumé des épisodes précédents
Nous avons vu que :
• les bugs sont une chose sérieuse
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Résumé des épisodes précédents
Nous avons vu que :
• les bugs sont une chose sérieuse
• l’interprétation abstraite permet de faire de la vérification, en faisant
des calculs sur des formes géométriques, qui approximent les
comportements du programme
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Résumé des épisodes précédents
Nous avons vu que :
• les bugs sont une chose sérieuse
• l’interprétation abstraite permet de faire de la vérification, en faisant
des calculs sur des formes géométriques, qui approximent les
comportements du programme
• les programmes utilisent (indirectement) des min et des max
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Résumé des épisodes précédents
Nous avons vu que :
• les bugs sont une chose sérieuse
• l’interprétation abstraite permet de faire de la vérification, en faisant
des calculs sur des formes géométriques, qui approximent les
comportements du programme
• les programmes utilisent (indirectement) des min et des max
Problème :
• les propriétés avec des min et max sont de nature disjonctive
max(x, y ) ≥ 2
équivaut à
x ≥ 2 ou y ≥ 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Résumé des épisodes précédents
Nous avons vu que :
• les bugs sont une chose sérieuse
• l’interprétation abstraite permet de faire de la vérification, en faisant
des calculs sur des formes géométriques, qui approximent les
comportements du programme
• les programmes utilisent (indirectement) des min et des max
Problème :
• les propriétés avec des min et max sont de nature disjonctive
max(x, y ) ≥ 2
équivaut à
x ≥ 2 ou y ≥ 2
• les techniques existantes en IA ne permettent pas bien d’approximer
ces propriétés.
Nous allons voir comment la géométrie tropicale peut apporter des
solutions à ce problème.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 21/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1)
1⊗1=
2⊕3=
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=
2⊕3=
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1
2⊕3=
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1=2
2⊕3=
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1=2
2 ⊕ 3 = max(2, 3)
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1=2
2 ⊕ 3 = max(2, 3) = 3
2⊗3=
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1=2
2 ⊕ 3 = max(2, 3) = 3
2⊗3=2+3
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale
Qu’est-ce que l’algèbre tropicale ?
1
Oubliez ce que vous avez appris à l’école primaire
2
l’addition ⊕ est maintenant l’opération max
3
la multiplication ⊗ correspond à l’opération +
1 ⊕ 1 = max(1, 1) = 1
1⊗1=1+1=2
2 ⊕ 3 = max(2, 3) = 3
2⊗3=2+3=5
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les tables de multiplication tropicale
Table de 9 :
9 ⊗ 1 = 9 + 1 = 10
9 ⊗ 2 = 9 + 2 = 11
9 ⊗ 3 = 9 + 3 = 12
9 ⊗ 4 = 9 + 4 = 13
9 ⊗ 5 = 9 + 5 = 14
9 ⊗ 6 = 9 + 6 = 15
9 ⊗ 7 = 9 + 7 = 16
9 ⊗ 8 = 9 + 8 = 17
9 ⊗ 9 = 9 + 9 = 18
9 ⊗ 10 = 9 + 10 = 19
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 23/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
• idem pour la multiplication :
3⊗4=4⊗3
1 ⊗ (3 ⊗ 7) = (1 ⊗ 3) ⊗ 7
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
• idem pour la multiplication :
3⊗4=4⊗3
1 ⊗ (3 ⊗ 7) = (1 ⊗ 3) ⊗ 7
• la multiplication est distributive par rapport à l’addition :
3 ⊗ (2 ⊗ 5) = (3 ⊗ 2) ⊕ (3 ⊗ 5)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
• idem pour la multiplication :
3⊗4=4⊗3
1 ⊗ (3 ⊗ 7) = (1 ⊗ 3) ⊗ 7
• la multiplication est distributive par rapport à l’addition :
3 ⊗ (2 ⊗ 5) = (3 ⊗ 2) ⊕ (3 ⊗ 5)
• il y a un “zero” et un “un” tropicaux : 0 := −∞, 1 := 0 :
3⊕0=3
4⊗1=1
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
• idem pour la multiplication :
3⊗4=4⊗3
1 ⊗ (3 ⊗ 7) = (1 ⊗ 3) ⊗ 7
• la multiplication est distributive par rapport à l’addition :
3 ⊗ (2 ⊗ 5) = (3 ⊗ 2) ⊕ (3 ⊗ 5)
• il y a un “zero” et un “un” tropicaux : 0 := −∞, 1 := 0 :
3⊕0=3
4⊗1=1
• il y a une division x y := x − y :
33=3−3=0=1
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre tropicale a une jolie structure
• l’addition est commutative et associative
2⊕3=3⊕2
2 ⊕ (3 ⊕ 4) = (2 ⊕ 3) ⊕ 4
• idem pour la multiplication :
3⊗4=4⊗3
1 ⊗ (3 ⊗ 7) = (1 ⊗ 3) ⊗ 7
• la multiplication est distributive par rapport à l’addition :
3 ⊗ (2 ⊗ 5) = (3 ⊗ 2) ⊕ (3 ⊗ 5)
• il y a un “zero” et un “un” tropicaux : 0 := −∞, 1 := 0 :
3⊕0=3
4⊗1=1
• il y a une division x y := x − y :
33=3−3=0=1
• MAIS il n’y a pas de soustraction :
1 ⊕ x = max(1, x) = 0 = −∞
Que pourrait valoir x ?
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Le président : J’ai trois super idées pour combler le déficit :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Le président : J’ai trois super idées pour combler le déficit :
1
contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Le président : J’ai trois super idées pour combler le déficit :
1
contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
2
taxe de 2.54 euros sur chaque entrée à Disneyland Paris
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Le président : J’ai trois super idées pour combler le déficit :
1
contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
2
taxe de 2.54 euros sur chaque entrée à Disneyland Paris
3
taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
Deux ministres
sont chez le président.
Le président : J’ai trois super idées pour combler le déficit :
1
contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
2
taxe de 2.54 euros sur chaque entrée à Disneyland Paris
3
taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
Combien en gros ça va rapporter ?
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 =
2.54 × 15 214 261 =
151.23 × 190 217 =
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
2.54 × 15 214 261 =
151.23 × 190 217 =
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000
2.54 × 15 214 261 =
151.23 × 190 217 =
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 =
151.23 × 190 217 =
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
2.54 × 15 214 261 =
≈ 10 × 10 000 000 = 100 000 000
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 =
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 =
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 =
≈ 100 × 100 000 = 10 000 000
Total =
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 =
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 =
≈ 100 × 100 000 = 10 000 000
Total =
Total ≈ 100 000 000
Temps de calcul : 2s
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 = 38 644 222.94
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 =
≈ 100 × 100 000 = 10 000 000
Total =
Total ≈ 100 000 000
Temps de calcul : 2s
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 = 38 644 222.94
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 = 28 766 516.91
≈ 100 × 100 000 = 10 000 000
Total =
Total ≈ 100 000 000
Temps de calcul : 2s
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur
• contribution forfaitaire de 12 euros pour chaque élève ou étudiant,
pour le désendettement futur de la France
• taxe de 2.54 euros sur chaque entrée à Disneyland Paris
• taxation des emplacements de camping 4 étoiles, 151.23 euros par
emplacement
12 × 14 998 462 = 179 981 544
≈ 10 × 10 000 000 = 100 000 000
2.54 × 15 214 261 = 38 644 222.94
≈ 1 × 10 000 000 = 10 000 000
151.23 × 190 217 = 28 766 516.91
≈ 100 × 100 000 = 10 000 000
Total = 247 392 283.85
Temps de calcul : 17s ! ! !
Total ≈ 100 000 000
Temps de calcul : 2s
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 26/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
10 × 10 000 000 = 100 000 000
1 × 10 000 000 = 10 000 000
100 × 100 000 = 10 000 000
Total ≈ 100 000 000
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 101+7
1 × 10 000 000 = 10 000 000
100 × 100 000 = 10 000 000
Total ≈ 100 000 000
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
1 × 10 000 000 = 10 000 000
100 × 100 000 = 10 000 000
Total ≈ 100 000 000
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
100 × 100 000 = 10 000 000
Total ≈ 100 000 000
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 100 000 000
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 10max(8,7,7)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 108
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 108
Autrement dit :
1⊗7=8
0⊗7=7
2⊗5=7
Total = 8 ⊕ 7 ⊕ 7 = 8
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 108
Le calcul est approximatif avec les puissances de 10, mais moins avec les
puissances de β, pour β choisi grand :
max(x, y ) ≤ logβ (β x + β y ) ≤ max(x, y ) + logβ 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des ordres de grandeur (2)
fait des calculs en algèbre tropicale :
101 × 107 = 108
100 × 107 = 107
102 × 105 = 107
Total ≈ 108
Le calcul est approximatif avec les puissances de 10, mais moins avec les
puissances de β, pour β choisi grand :
max(x, y ) ≤ logβ (β x + β y ) ≤ max(x, y ) + logβ 2
logβ (β x × β y ) = x + y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 27/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins
Paris
33
Saint-Cyr 10
26
Versailles
12
16
18
Antony
21
12
Montigny
Saclay
18
12
Massy
10
Magny
11
9
Palaiseau
11
12
Saint-Rémy
12
10
Gif
9
Orsay
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 28/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins
Paris
33
Saint-Cyr 10
26
Versailles
12
16
18
Antony
21
12
Montigny
Saclay
18
12
Massy
10
Magny
11
9
Palaiseau
11
12
Saint-Rémy
12
10
Gif
9
Orsay
Le plus court chemin entre de Massy à Magny est donné par :
min(dSaclay-Magny + 12, dPal.-Magny + 9, dVer.-Magny + 21, dAntony-Magny + 12)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 28/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins
Paris
33
Saint-Cyr 10
26
Versailles
12
16
18
Antony
21
12
Montigny
Saclay
18
12
Massy
10
Magny
11
9
Palaiseau
11
12
Saint-Rémy
12
10
Gif
9
Orsay
L’opposé du plus court chemin est donné par :
max(−dSaclay-Magny −12, −dPal.-Magny −9, −dVer.-Magny −21, −dAntony-Magny −12)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 28/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins
Paris
33
Saint-Cyr 10
26
Versailles
12
16
18
Antony
21
12
Montigny
Saclay
18
12
Massy
10
Magny
11
9
Palaiseau
11
12
Saint-Rémy
12
10
Gif
9
Orsay
L’opposé du plus court chemin est donné par :
(−12) ⊗ (−dSaclay-Magny ) ⊕ (−9) ⊗ (−dPal.-Magny )
⊕ (−21) ⊗ (−dVer.-MagnyPas
) d’erreurs
⊕ (−12)
⊗ (−dAntony-Magny )
fatales avec le tropical ! — Xavier Allamigeon — 28/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins (2)
Plus généralement, si A est la matrice composée de l’opposé des
distances :
Aij = opposé de la distance entre les villes i et j
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 29/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins (2)
Plus généralement, si A est la matrice composée de l’opposé des
distances :
Aij = opposé de la distance entre les villes i et j
alors l’opposé des plus courts chemins est donné par la matrice
A∗ = A0 ⊕ A1 ⊕ A2 ⊕ . . .
où An = A ⊗ A ⊗ · · · ⊗ A représente les plus courts chemins de longueurs
{z
}
|
n fois
au plus n.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 29/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
L’algèbre des plus courts chemins (2)
Plus généralement, si A est la matrice composée de l’opposé des
distances :
Aij = opposé de la distance entre les villes i et j
alors l’opposé des plus courts chemins est donné par la matrice
A∗ = A0 ⊕ A1 ⊕ A2 ⊕ · · · ⊕ AN
où An = A ⊗ A ⊗ · · · ⊗ A représente les plus courts chemins de longueurs
{z
}
|
n fois
au plus n.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 29/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 30/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite
y
A = (3, 4)
B = (7, 2)
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 31/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite
Le segment entre A et B est formé des barycentres λ × A + µ × B, où
λ, µ sont positifs, et λ + µ = 1. Ici :
λ × (3, 4) + µ × (7, 2) = (3λ + 7µ, 4λ + 2µ)
y
A = (3, 4)
B = (7, 2)
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 31/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite
Le segment entre A et B est formé des barycentres λ × A + µ × B, où
λ, µ sont positifs, et λ + µ = 1. Ici :
λ × (3, 4) + µ × (7, 2) = (3λ + 7µ, 4λ + 2µ)
y
(3., 4.)
λ = 1., µ = 0.
A = (3, 4)
B = (7, 2)
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 31/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (2)
Le segment tropical entre A et B est formé des barycentres
λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici :
λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) )
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (2)
Le segment tropical entre A et B est formé des barycentres
λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici :
λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) )
• la condition de positivité λ, µ ≥ 0 = −∞ est toujours satisfaite,
• λ ⊕ µ = 1 revient à dire que max(λ, µ) = 0, soit λ, µ ≤ 0, et l’un
des deux doit être nul !
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (2)
Le segment tropical entre A et B est formé des barycentres
λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici :
λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) )
y
A = (3, 4)
B = (7, 2)
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (2)
Le segment tropical entre A et B est formé des barycentres
λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici :
λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) )
y
(3., 4.)
λ = 0., µ = −4.
A = (3, 4)
B = (7, 2)
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (3)
y
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 33/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (3)
y
B0
A0
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 33/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas du segment de droite (3)
y
B 00
A00
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 33/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les triangles tropicaux (2)
y
C
A
B
x
Plus généralement, les hyperrectangles en dimension n sont des simplexes
tropicaux, i.e. des enveloppes tropicalement convexes de n + 1 points.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
aX + bY + c = 0
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
La droite tropicale est donnée par l’égalité sur les ordres de grandeurs
X = Θ(β x ) Y = Θ(β y )
pour β grand
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
La droite tropicale est donnée par l’égalité sur les ordres de grandeurs
X = Θ(β x ) Y = Θ(β y )
pour β grand
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
La droite tropicale est donnée par l’égalité sur les ordres de grandeurs
X = Θ(β x ) Y = Θ(β y )
pour β grand
On regarde la droite X + Y + 1 = 0 avec des “lunettes logarithmiques”,
i.e. son image par l’application (X , Y ) 7→ (logβ |X |, logβ |Y |)
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
La droite tropicale est donnée par l’égalité sur les ordres de grandeurs
X = Θ(β x ) Y = Θ(β y )
pour β grand
On regarde la droite X + Y + 1 = 0 avec des “lunettes logarithmiques”,
i.e. son image par l’application (X , Y ) 7→ (logβ |X |, logβ |Y |)
y
La droite tropicale est le
“squelette” de l’amibe (β → +∞).
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Le cas des droites
Une droite classique :
X +Y +1=0
La droite tropicale est donnée par l’égalité sur les ordres de grandeurs
X = Θ(β x ) Y = Θ(β y )
pour β grand
On regarde la droite X + Y + 1 = 0 avec des “lunettes logarithmiques”,
i.e. son image par l’application (X , Y ) 7→ (logβ |X |, logβ |Y |)
y
La droite tropicale est le
“squelette” de l’amibe (β → +∞).
x
Elle est donnée par les points (x, y )
tels que le maximum
max(x, y , 0)
est atteint deux fois.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces
Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en
dimension 2).
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces
Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en
dimension 2).
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces
Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en
dimension 2).
y
x
Un demi-espace est défini par une inégalité affine, ici :
y ≥ (1/3) × x + 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces (2)
Une droite tropicale sépare le plan en 3 secteurs.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces (2)
Une droite tropicale sépare le plan en 3 secteurs.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces (2)
Une droite tropicale sépare le plan en 3 secteurs.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces (2)
Une droite tropicale sépare le plan en 3 secteurs.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les demi-espaces (2)
Une droite tropicale sépare le plan en 3 secteurs.
y
x
• les demi-espaces sont obtenus en sélectionnant 1 ou 2 secteurs
• ils correspondent aux solutions d’inégalités tropicalement affines
(−4) ⊗ y ≤ (−5) ⊗ x ⊕ 0
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres (convexes)
On les utilisent depuis la maternelle : les triangles, les carrés, les
rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc.
y
x
Ils sont donnés par les solutions de plusieurs inégalités (affines) :
2≤x ≤6
2≤y ≤6
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux
Ils sont donnés par les solutions de plusieurs inégalités (affines)
tropicales :
x ≤y ⊕0
0≤2⊗x
x ≤2
0 ≤ x ⊕ (−1) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 40/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux
Ils sont donnés par les solutions de plusieurs inégalités (affines)
tropicales :
x ≤y ⊕0
0≤2⊗x
x ≤2
0 ≤ x ⊕ (−1) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 40/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux
Ils sont donnés par les solutions de plusieurs inégalités (affines)
tropicales :
x ≤y ⊕0
0≤2⊗x
x ≤2
0 ≤ x ⊕ (−1) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 40/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux
Ils sont donnés par les solutions de plusieurs inégalités (affines)
tropicales :
x ≤y ⊕0
0≤2⊗x
x ≤2
0 ≤ x ⊕ (−1) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 40/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux
Ils sont donnés par les solutions de plusieurs inégalités (affines)
tropicales :
x ≤y ⊕0
0≤2⊗x
x ≤2
0 ≤ x ⊕ (−1) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 40/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux (2)
Ils permettent de représenter les propriétés avec min et max qu’on
souhaite vérifier sur les programmes.
Exemple :
n
min(len dst, n) = min(len src, n)
revient à :
max(−len dst, −n) ≤ max(−len src, −n)
lendst
max(−len src, −n) ≤ max(−len dst, −n) lensrc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 41/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux (2)
Ils permettent de représenter les propriétés avec min et max qu’on
souhaite vérifier sur les programmes.
Exemple :
n
min(len dst, n) = min(len src, n)
revient à :
max(−len dst, −n) ≤ max(−len src, −n)
lendst
max(−len src, −n) ≤ max(−len dst, −n) lensrc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 41/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux (2)
Ils permettent de représenter les propriétés avec min et max qu’on
souhaite vérifier sur les programmes.
Exemple :
n
min(len dst, n) = min(len src, n)
revient à :
(−len dst) ⊕ (−n) ≤ (−len src) ⊕ (−n)
lendst
(−len src) ⊕ (−n) ≤ (−len dst) ⊕ (−n) lensrc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 41/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Les polyèdres tropicaux (2)
Ils permettent de représenter les propriétés avec min et max qu’on
souhaite vérifier sur les programmes.
Exemple :
n
Idée : vérifier des programmes, en faisant
min(len dst, n) = min(len src, n)
des calculs sur les polyèdres tropicaux
revient à :
(−len dst) ⊕ (−n) ≤ (−len src) ⊕ (−n)
lendst
(−len src) ⊕ (−n) ≤ (−len dst) ⊕ (−n) lensrc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 41/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 42/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Déterminer si un polyèdre est vide . . .
Considérons le polyèdre tropical :
−3 + y ≤ x
0 ≤ max(−4 + x, −6 + y )
−2 ≤ y
−2 + x ≤ max(−2 + y , 0)
Question : existe-t-il une solution à ces inégalités ?
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 43/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 :
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 : Max gagne 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 : Max gagne 2 + 0 = 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 : Max gagne 2 + 0 + 0 = 2
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 : Max gagne 2 + 0 + 0 + (−4) = −2 :-(
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . et jouer à un jeu . . .
Min et Max jouent à un jeu sur un graphe :
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Mode d’emploi :
• les joueurs bougent alternativement un pion sur les nœuds
• quand le pion est sur un nœud “cercle”, Min choisit un arc sortant,
et paye à Max le montant indiqué sur l’arc
• quand le pion est sur un nœud “carré”, Max choisit un arc sortant,
et reçoit de Min un paiement du montant indiqué sur l’arc
En partant du nœud cercle 1 :
Max gagne 2 + (−2) + 3 + 0 = 3 :-)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
1
0
2
3
2
−4
1
2
3
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
. . . c’est la même chose
Les deux joueurs Min et Max jouent un nombre infini de fois... On
regarde leur gain (ou perte) moyen par tour.
Théorème (Akian, Gaubert, Guterman)
Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir
du noeud “cercle” 3, le joueur Max gagne.
Parenthèse théorique :
• décider si Max peut
1 gagner
2 est dans3NP ∩ coNP
3
• l’existence d’un algorithme polynomial est un problème
ouvert 0
2
−4
1
2
−6 0
2
0
3
−2
0
4
En suivant le cycle en bleu, Max gagne 3$ à coup sûr.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
C
A
x
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P
C
A
x
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P
C
Q
A
x
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P
C
Q = A ⊕ (−1)B
Q = A ⊕ (−1)B
A
x
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P = Q ⊕ (−1)D
C
Q = A ⊕ (−1)B
Q
A
x
P = Q ⊕ (−1)D
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P = Q ⊕ (−1)D
C
Q = A ⊕ (−1)B
Q
A
x
P = Q ⊕ (−1)D
= (1)A ⊕ (−1)B ⊕ (−1)D
B
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical
Un polyèdre tropical peut être aussi décrit par ses sommets.
y
D
P = Q ⊕ (−1)D
C
Q = A ⊕ (−1)B
Q
A
x
P = Q ⊕ (−1)D
= (1)A ⊕ (−1)B ⊕ (−1)D
B
Tout point du polyèdre peut être écrit comme un barycentre des
sommets.
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (2)
Certaines opérations sont faciles à faire avec la représentation par
inégalités : intersection
y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 47/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (2)
Certaines opérations sont faciles à faire avec la représentation par
inégalités : intersection
y
x ≤y ⊕0
0≤2⊗x
x ⊕ (−2) ⊗ y ≤ 2
0 ≤ x ⊕ (−1) ⊗ y
x
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 47/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (2)
Certaines opérations sont faciles à faire avec la représentation par
inégalités : intersection
y
x ≤y ⊕0
0≤2⊗x
x ⊕ (−2) ⊗ y ≤ 2
0 ≤ x ⊕ (−1) ⊗ y
x
0 ≤ 1 ⊗ x ⊕ (−2) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 47/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (2)
Certaines opérations sont faciles à faire avec la représentation par
inégalités : intersection
y
x ≤y ⊕0
0≤2⊗x
x ⊕ (−2) ⊗ y ≤ 2
0 ≤ x ⊕ (−1) ⊗ y
x
0 ≤ 1 ⊗ x ⊕ (−2) ⊗ y
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 47/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (3)
D’autres opérations sont difficiles, mais faciles sur les sommets : union
(approchée)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (3)
D’autres opérations sont difficiles, mais faciles sur les sommets : union
(approchée)
y
x
• l’union de deux polyèdres n’est pas un polyèdre (en général)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (3)
D’autres opérations sont difficiles, mais faciles sur les sommets : union
(approchée)
y
x
• l’union de deux polyèdres n’est pas un polyèdre (en général)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (3)
D’autres opérations sont difficiles, mais faciles sur les sommets : union
(approchée)
y
x
• l’union de deux polyèdres n’est pas un polyèdre (en général)
• on sur-approxime par l’enveloppe convexe de l’union
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Calculer les sommets d’un polyèdre tropical (3)
D’autres opérations sont difficiles, mais faciles sur les sommets : union
(approchée)
y
Calculer les sommets d’un polyèdre
tropical est un problème fondamental
x
• l’union de deux polyèdres n’est pas un polyèdre (en général)
• on sur-approxime par l’enveloppe convexe de l’union
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 49/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Application à la vérification
On sur-approxime la sémantique d’un programme grâce à des polyèdres
tropicaux :
v2
v1
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Application à la vérification
On sur-approxime la sémantique d’un programme grâce à des polyèdres
tropicaux :
v2
v1
En pratique :
• la vérification de programme est réalisée grâce aux algorithmes
qu’on a définis sur les polyèdres tropicaux
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Application à la vérification
On sur-approxime la sémantique d’un programme grâce à des polyèdres
tropicaux :
v2
v1
En pratique :
• la vérification de programme est réalisée grâce aux algorithmes
qu’on a définis sur les polyèdres tropicaux
• c’est implémenté → TPLib, sous licence LGPL
(https://gforge.inria.fr/projects/tplib)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Application à la vérification
On sur-approxime la sémantique d’un programme grâce à des polyèdres
tropicaux :
v2
v1
En pratique :
• la vérification de programme est réalisée grâce aux algorithmes
qu’on a définis sur les polyèdres tropicaux
• c’est implémenté → TPLib, sous licence LGPL
(https://gforge.inria.fr/projects/tplib)
• ça fonctionne pour de vrai → DEMO
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Plan de l’exposé
1 La vérification de programmes par interprétation abstraite
2 Des programmes avec des min et des max
3 L’algèbre tropicale
4 La géométrie tropicale
5 Faire des calculs sur les polyèdres tropicaux
6 Application à la vérification
7 Conclusion
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 51/53
La vérification
Progs avec min/max
L’algèbre tropicale
La géométrie tropicale
Calculs polyèdres tropicaux
Appli à la vérif
Conclusion
Conclusion
Contribution à la frontière entre les mathématiques et l’informatique :
• la géométrie tropicale apporte de nouvelles approches en
vérification :
• verif de programmes
• aussi de systèmes temps-réels
• soulève aussi de très nombreuses questions théoriques
• inventer les algorithmes en géométrie tropicale
• mieux comprendre les propriétés de ces objets (TPLib connecté à
Polymake www.polymake.org)
Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 52/53
Merci !

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Top types

Top brands

Download Pas d`erreurs fatales avec le tropical ! - Unithé ou café