Download Pas d`erreurs fatales avec le tropical ! - Unithé ou café
Transcript
La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Pas d’erreurs fatales avec le tropical ! Unithé ou café Xavier Allamigeon INRIA Saclay – Ile-de-France et CMAP Ecole Polytechnique, équipe MAXPLUS [email protected] 9 mars 2012 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 1/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’équipe MAXPLUS Commune avec le CMAP de l’X, sur le platâl (aile 0 des labos) • permanents : Sté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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion But de cet exposé Vous montrer le lien entre : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 3/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion But de cet exposé Vous montrer le lien entre : • la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion But de cet exposé Vous montrer le lien entre : • la vérification de programmes • la géomé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 4/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 5/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les bugs font partie de notre quotidien Leur forme évolue avec le temps : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les bugs font partie de notre quotidien Leur forme évolue avec le temps : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les bugs font partie de notre quotidien En grand, à Times square : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les bugs font partie de notre quotidien Longue tradition à la SNCF : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 6/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion On met du logiciel partout Y compris dans des endroits critiques : Ce qui mène parfois à : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 7/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes Cela consiste à développer des outils d’analyse statique de logiciels : • apportant l’assurance qu’il n’y a pas de bogues • (presque) entièrement automatiques • capables de s’attaquer à de très gros codes Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 8/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes Cela consiste à développer des outils d’analyse statique de logiciels : • apportant l’assurance qu’il n’y a pas de bogues • (presque) entièrement automatiques • capables de s’attaquer à de très gros codes Quels genres de bugs ? • division par zero : 1/0 retourne une erreur • dépassement de capacité 15561676378226 ∗ 387326762373690 = −2585705764785308204 • etc =⇒ les outils de vérification de logiciels doivent en fait s’assurer que certaines bonnes propriétés sont satisfaites. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 8/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vé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 interprétation abstraite (Cousot & Cousot) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 9/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; • à la ligne 1, x vaut 0 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; • à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; • à la ligne 1, x vaut 0 • comme x est plus petit que 5, on rentre dans la boucle • à la ligne 3, x vaut 2, Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; • à la ligne 1, x vaut 0 • comme x est plus petit que 5, on rentre dans la boucle • à la ligne 3, x vaut 2, puis 4, Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; • à la ligne 1, x vaut 0 • comme x est plus petit que 5, on rentre dans la boucle • à la ligne 3, x vaut 2, puis 4, puis 6 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; à la ligne 1, x vaut 0 comme x est plus petit que 5, on rentre dans la boucle à la ligne 3, x vaut 2, puis 4, puis 6 on sort de la boucle, on saute à la ligne 5 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite La sémantique d’un programme décrit l’ensemble de tous les comportements possibles du programme. Exemple trè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; à la ligne 1, x vaut 0 comme x est plus petit que 5, on rentre dans la boucle à la ligne 3, x vaut 2, puis 4, puis 6 on sort de la boucle, on saute à la ligne 5 à la ligne 5, x vaut 6, et y vaut 1/6 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 10/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général ligne 1 ligne 2 ligne 3 ligne 4 ligne 5 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général ligne 1 ligne 2 ligne 3 ligne 4 ligne 5 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général • et pourtant on en aurait besoin pour dé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général • et pourtant on en aurait besoin pour dé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 sémantique Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général • et pourtant on en aurait besoin pour dé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 sémantique • on ne peut rater aucun bug Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 11/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion La vérification de programmes par interprétation abstraite (2) • la sémantique d’un programme n’est pas calculable en général • et pourtant on en aurait besoin pour dé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 sémantique • on ne peut rater aucun bug • mais si on n’est pas assez pré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course Exemple de sur-approximations : les intervalles −→ on encadre chaque variable entre deux constantes En pratique : 1 : si [condition alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 aprè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 après la ligne 6 : 6 : si y >= 3 alors 7: x := x+1; 0≤x≤5 3≤y≤5 • à la ligne 7 : 1≤x≤6 3≤y≤5 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 12/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course Exemple de sur-approximations : les intervalles −→ on encadre chaque variable entre deux constantes En pratique : 1 : si [condition alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course Exemple de sur-approximations : les intervalles −→ on encadre chaque variable entre deux constantes En pratique : Juste après la ligne 6 : 1 : si [condition alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course Exemple de sur-approximations : les intervalles −→ on encadre chaque variable entre deux constantes En pratique : Juste après la ligne 6 : 1 : si [condition alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 alé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interpré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) . . . qui offrent différents niveaux de précision y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) . . . qui offrent différents niveaux de précision y • intervalles x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) . . . qui offrent différents niveaux de précision y • intervalles • zones x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) . . . qui offrent différents niveaux de précision y • intervalles • zones • polyèdres convexes x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’interprétation abstraite : crash course (2) Il y a plusieurs moyens d’approximer, par exemple : • intervals 1 ≤ x ≤ 3 (Cousot & Cousot) • zones y − x ≥ 1 (Miné) • polyèdres convexes 2x + 5y ≥ −3 (Cousot & Halbwachs) . . . qui offrent différents niveaux de précision y • intervalles • zones • polyèdres convexes x Problème : certaines propriétés sont difficiles à approcher Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 13/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 14/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le B.A.-BA : les algorithmes de tris Le tri pair-impair : 5 −3 −7 −3 2 0 Blocs élé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le B.A.-BA : les algorithmes de tris Le tri pair-impair : 5 −3 2 Blocs élémentaires : 4 0 8 1 −7 3 1 2 5 1 3 2 5 A la sortie, • l’élément le plus à gauche est le minimum • l’élément le plus à droite est le maximum des éléments données en entrée. −7 −3 0 1 2 4 5 8 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 15/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Synthèse de plusieurs capteurs Plusieurs capteurs pour mesurer la décélération : L’airbag se déclenche dès qu’un des capteurs mesure une trop grande décélération : max(d1 , d2 , d3 ) ≥ dmax Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 16/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Synthèse de plusieurs capteurs (2) En réalité, c’est plus compliqué −→ triplex sensor voter (Dierkes, Cofer, Ervin, Miller, TAPAS 2010) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 17/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Synthèse de plusieurs capteurs (2) En réalité, c’est plus compliqué −→ triplex sensor voter (Dierkes, Cofer, Ervin, Miller, TAPAS 2010) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 17/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Synthèse de plusieurs capteurs (2) En réalité, c’est plus compliqué −→ triplex sensor voter Propriétés à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Il faut manipuler la mémoire avec précaution Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Il faut manipuler la mémoire avec précaution −→ attention aux buffer overflows Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Il faut manipuler la mémoire avec précaution −→ attention aux buffer overflows Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Il faut manipuler la mémoire avec précaution −→ attention aux buffer overflows Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire C’est l’utilisation, en programmation, de • tableaux, matrices • chaı̂nes de caractères ("Hello World!" ) • listes, arbres, etc =⇒ largement utilisé dans les langages de programmation moderne : C, C++, Java, etc Il faut manipuler la mémoire avec précaution −→ attention aux buffer overflows Les buffer overflows peuvent provoquer : • un plantage de la machine (SEGFAULT) • des trous de sécurité Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 18/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 caractères est-elle codé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Manipulations de mémoire (2) memcpy(dst,src,n) copie les n premiers caractè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Résumé des épisodes précédents Nous avons vu que : • les bugs sont une chose sérieuse Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Résumé des épisodes précédents Nous avons vu que : • les bugs sont une chose sérieuse • l’interprétation abstraite permet de faire de la vérification, en faisant des calculs sur des formes géométriques, qui approximent les comportements du programme Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Résumé des épisodes précédents Nous avons vu que : • les bugs sont une chose sérieuse • l’interprétation abstraite permet de faire de la vérification, en faisant des calculs sur des formes géomé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Résumé des épisodes précédents Nous avons vu que : • les bugs sont une chose sérieuse • l’interprétation abstraite permet de faire de la vérification, en faisant des calculs sur des formes géométriques, qui approximent les comportements du programme • les programmes utilisent (indirectement) des min et des max Problème : • les propriétés avec des min et max sont de nature disjonctive max(x, y ) ≥ 2 équivaut à x ≥ 2 ou y ≥ 2 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Résumé des épisodes précédents Nous avons vu que : • les bugs sont une chose sérieuse • l’interprétation abstraite permet de faire de la vérification, en faisant des calculs sur des formes géométriques, qui approximent les comportements du programme • les programmes utilisent (indirectement) des min et des max Problème : • les propriétés avec des min et max sont de nature disjonctive max(x, y ) ≥ 2 équivaut à x ≥ 2 ou y ≥ 2 • les techniques existantes en IA ne permettent pas bien d’approximer ces propriétés. Nous allons voir comment la géométrie tropicale peut apporter des solutions à ce problème. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 20/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 21/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opération + Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opération + 1 ⊕ 1 = max(1, 1) 1⊗1= 2⊕3= 2⊗3= Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 22/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre tropicale Qu’est-ce que l’algèbre tropicale ? 1 Oubliez ce que vous avez appris à l’école primaire 2 l’addition ⊕ est maintenant l’opération max 3 la multiplication ⊗ correspond à l’opé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 à l’addition : 3 ⊗ (2 ⊗ 5) = (3 ⊗ 2) ⊕ (3 ⊗ 5) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 24/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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 à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Le président : J’ai trois super idées pour combler le déficit : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Le président : J’ai trois super idées pour combler le déficit : 1 contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Le président : J’ai trois super idées pour combler le déficit : 1 contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France 2 taxe de 2.54 euros sur chaque entrée à Disneyland Paris Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Le président : J’ai trois super idées pour combler le déficit : 1 contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France 2 taxe de 2.54 euros sur chaque entrée à Disneyland Paris 3 taxation des emplacements de camping 4 étoiles, 151.23 euros par emplacement Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur Deux ministres sont chez le président. Le président : J’ai trois super idées pour combler le déficit : 1 contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France 2 taxe de 2.54 euros sur chaque entrée à Disneyland Paris 3 taxation des emplacements de camping 4 étoiles, 151.23 euros par emplacement Combien en gros ça va rapporter ? Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 25/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur • contribution forfaitaire de 12 euros pour chaque élève ou étudiant, pour le désendettement futur de la France • taxe de 2.54 euros sur chaque entrée à Disneyland Paris • taxation des emplacements de camping 4 é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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des ordres de grandeur (2) fait des calculs en algè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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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-Rémy 12 10 Gif 9 Orsay Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 28/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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-Rémy 12 10 Gif 9 Orsay Le plus court chemin entre de Massy à Magny est donné 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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-Rémy 12 10 Gif 9 Orsay L’opposé du plus court chemin est donné 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algè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-Rémy 12 10 Gif 9 Orsay L’opposé du plus court chemin est donné par : (−12) ⊗ (−dSaclay-Magny ) ⊕ (−9) ⊗ (−dPal.-Magny ) ⊕ (−21) ⊗ (−dVer.-MagnyPas ) d’erreurs ⊕ (−12) ⊗ (−dAntony-Magny ) fatales avec le tropical ! — Xavier Allamigeon — 28/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des plus courts chemins (2) Plus généralement, si A est la matrice composée de l’opposé des distances : Aij = opposé de la distance entre les villes i et j Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 29/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des plus courts chemins (2) Plus généralement, si A est la matrice composée de l’opposé des distances : Aij = opposé de la distance entre les villes i et j alors l’opposé des plus courts chemins est donné par la matrice A∗ = A0 ⊕ A1 ⊕ A2 ⊕ . . . où An = A ⊗ A ⊗ · · · ⊗ A repré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion L’algèbre des plus courts chemins (2) Plus généralement, si A est la matrice composée de l’opposé des distances : Aij = opposé de la distance entre les villes i et j alors l’opposé des plus courts chemins est donné par la matrice A∗ = A0 ⊕ A1 ⊕ A2 ⊕ · · · ⊕ AN où An = A ⊗ A ⊗ · · · ⊗ A repré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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 30/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite Le segment entre A et B est formé des barycentres λ × A + µ × B, où λ, µ 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite Le segment entre A et B est formé des barycentres λ × A + µ × B, où λ, µ 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite (2) Le segment tropical entre A et B est formé des barycentres λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici : λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) ) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite (2) Le segment tropical entre A et B est formé des barycentres λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 1. Ici : λ ⊗ (3, 4) ⊕ µ ⊗ (7, 2) = ( max(3 + λ, 7 + µ) , max(4 + λ, 2 + µ) ) • la condition de positivité λ, µ ≥ 0 = −∞ est toujours satisfaite, • λ ⊕ µ = 1 revient à dire que max(λ, µ) = 0, soit λ, µ ≤ 0, et l’un des deux doit être nul ! Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 32/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite (2) Le segment tropical entre A et B est formé des barycentres λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas du segment de droite (2) Le segment tropical entre A et B est formé des barycentres λ ⊗ A ⊕ µ ⊗ B, où λ ⊕ µ = 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 34/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 35/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les triangles tropicaux (2) y C A B x Plus géné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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas des droites Une droite classique : X +Y +1=0 La droite tropicale est donnée par l’égalité sur les ordres de grandeurs X = Θ(β x ) Y = Θ(β y ) pour β grand Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas des droites Une droite classique : X +Y +1=0 La droite tropicale est donnée par l’égalité sur les ordres de grandeurs X = Θ(β x ) Y = Θ(β y ) pour β grand Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 36/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas des droites Une droite classique : X +Y +1=0 La droite tropicale est donnée par l’égalité 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas des droites Une droite classique : X +Y +1=0 La droite tropicale est donnée par l’égalité 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Le cas des droites Une droite classique : X +Y +1=0 La droite tropicale est donnée par l’égalité 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 donné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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en dimension 2). y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en dimension 2). y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces Ils sont définis comme les ensembles situés “d’un côté” d’une droite (en dimension 2). y x Un demi-espace est défini par une inégalité affine, ici : y ≥ (1/3) × x + 2 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 37/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces (2) Une droite tropicale sépare le plan en 3 secteurs. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces (2) Une droite tropicale sépare le plan en 3 secteurs. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces (2) Une droite tropicale sépare le plan en 3 secteurs. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces (2) Une droite tropicale sépare le plan en 3 secteurs. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les demi-espaces (2) Une droite tropicale sépare le plan en 3 secteurs. y x • les demi-espaces sont obtenus en sélectionnant 1 ou 2 secteurs • ils correspondent aux solutions d’inégalités tropicalement affines (−4) ⊗ y ≤ (−5) ⊗ x ⊕ 0 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 38/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres (convexes) On les utilisent depuis la maternelle : les triangles, les carrés, les rectangles, les losanges, les trapèzes, certains pentagones, hexagones, etc. y x Ils sont donnés par les solutions de plusieurs inégalités (affines) : 2≤x ≤6 2≤y ≤6 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 39/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux Ils sont donnés par les solutions de plusieurs inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux Ils sont donnés par les solutions de plusieurs inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux Ils sont donnés par les solutions de plusieurs inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux Ils sont donnés par les solutions de plusieurs inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux Ils sont donnés par les solutions de plusieurs inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux (2) Ils permettent de représenter les propriétés avec min et max qu’on souhaite vérifier sur les programmes. Exemple : n min(len dst, n) = min(len src, n) revient à : 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux (2) Ils permettent de représenter les propriétés avec min et max qu’on souhaite vérifier sur les programmes. Exemple : n min(len dst, n) = min(len src, n) revient à : 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux (2) Ils permettent de représenter les propriétés avec min et max qu’on souhaite vérifier sur les programmes. Exemple : n min(len dst, n) = min(len src, n) revient à : (−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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Les polyèdres tropicaux (2) Ils permettent de représenter les propriétés avec min et max qu’on souhaite vérifier sur les programmes. Exemple : n Idée : vérifier des programmes, en faisant min(len dst, n) = min(len src, n) des calculs sur les polyèdres tropicaux revient à : (−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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 42/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Déterminer si un polyèdre est vide . . . Considérons le polyè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 à ces inégalités ? Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 43/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué sur l’arc Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué sur l’arc En partant du nœud cercle 1 : Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 44/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . et jouer à un jeu . . . Min et Max jouent à 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 à Max le montant indiqué sur l’arc • quand le pion est sur un nœud “carré”, Max choisit un arc sortant, et reçoit de Min un paiement du montant indiqué 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la mê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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à 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$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion . . . c’est la même chose Les deux joueurs Min et Max jouent un nombre infini de fois... On regarde leur gain (ou perte) moyen par tour. Théorème (Akian, Gaubert, Guterman) Le polyèdre est non-vide si, et seulement si, en débutant le jeu à partir du noeud “cercle” 3, le joueur Max gagne. Parenthèse théorique : • décider si Max peut 1 gagner 2 est dans3NP ∩ coNP 3 • l’existence d’un algorithme polynomial est un problème ouvert 0 2 −4 1 2 −6 0 2 0 3 −2 0 4 En suivant le cycle en bleu, Max gagne 3$ à coup sûr. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 45/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi décrit par ses sommets. y D C A x B Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi décrit par ses sommets. y D P C A x B Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi décrit par ses sommets. y D P C Q A x B Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi dé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi dé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi dé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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical Un polyèdre tropical peut être aussi dé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 polyèdre peut être écrit comme un barycentre des sommets. Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 46/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (2) Certaines opérations sont faciles à faire avec la représentation par inégalités : intersection y x Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 47/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (2) Certaines opérations sont faciles à faire avec la représentation par inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (2) Certaines opérations sont faciles à faire avec la représentation par inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (2) Certaines opérations sont faciles à faire avec la représentation par inégalité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 vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (3) D’autres opérations sont difficiles, mais faciles sur les sommets : union (approchée) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (3) D’autres opérations sont difficiles, mais faciles sur les sommets : union (approchée) y x • l’union de deux polyèdres n’est pas un polyèdre (en général) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (3) D’autres opérations sont difficiles, mais faciles sur les sommets : union (approchée) y x • l’union de deux polyèdres n’est pas un polyèdre (en général) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (3) D’autres opérations sont difficiles, mais faciles sur les sommets : union (approchée) y x • l’union de deux polyèdres n’est pas un polyèdre (en général) • on sur-approxime par l’enveloppe convexe de l’union Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Calculer les sommets d’un polyèdre tropical (3) D’autres opérations sont difficiles, mais faciles sur les sommets : union (approchée) y Calculer les sommets d’un polyèdre tropical est un problème fondamental x • l’union de deux polyèdres n’est pas un polyèdre (en général) • on sur-approxime par l’enveloppe convexe de l’union Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 48/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 49/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Application à la vérification On sur-approxime la sémantique d’un programme grâce à des polyèdres tropicaux : v2 v1 Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Application à la vérification On sur-approxime la sémantique d’un programme grâce à des polyèdres tropicaux : v2 v1 En pratique : • la vérification de programme est réalisée grâce aux algorithmes qu’on a définis sur les polyèdres tropicaux Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Application à la vérification On sur-approxime la sémantique d’un programme grâce à des polyèdres tropicaux : v2 v1 En pratique : • la vérification de programme est réalisée grâce aux algorithmes qu’on a définis sur les polyèdres tropicaux • c’est implémenté → TPLib, sous licence LGPL (https://gforge.inria.fr/projects/tplib) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Application à la vérification On sur-approxime la sémantique d’un programme grâce à des polyèdres tropicaux : v2 v1 En pratique : • la vérification de programme est réalisée grâce aux algorithmes qu’on a définis sur les polyèdres tropicaux • c’est implémenté → TPLib, sous licence LGPL (https://gforge.inria.fr/projects/tplib) • ça fonctionne pour de vrai → DEMO Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 50/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Plan de l’exposé 1 La vérification de programmes par interprétation abstraite 2 Des programmes avec des min et des max 3 L’algèbre tropicale 4 La géométrie tropicale 5 Faire des calculs sur les polyèdres tropicaux 6 Application à la vérification 7 Conclusion Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 51/53 La vérification Progs avec min/max L’algèbre tropicale La géométrie tropicale Calculs polyèdres tropicaux Appli à la vérif Conclusion Conclusion Contribution à la frontière entre les mathématiques et l’informatique : • la géométrie tropicale apporte de nouvelles approches en vérification : • verif de programmes • aussi de systèmes temps-réels • soulève aussi de très nombreuses questions théoriques • inventer les algorithmes en géométrie tropicale • mieux comprendre les propriétés de ces objets (TPLib connecté à Polymake www.polymake.org) Pas d’erreurs fatales avec le tropical ! — Xavier Allamigeon — 52/53 Merci !