Yves BERTOT
Articles de cet auteur
Nov 20 2013
Soutenance de Thèse : Étude formelle d’algorithmes efficaces en algèbre linéaire
Le mercredi 20/11/2013, à partir de 13h30 à la salle de conférence I3S.
Orateur : Maxime Denès.
Titre : Étude formelle d’algorithmes efficaces en algèbre linéaire.
Résumé : Les méthodes formelles ont atteint un degré de maturité conduisant à la
conception de systèmes de preuves généralistes, permettant à la fois de
vérifier la correction de systèmes logiciels complexes ou de formaliser des
mathématiques avancées. Mais souvent, l’accent est mis davantage sur la
facilité du raisonnement sur les programmes plutôt que sur leur exécution
efficace. L’antagonisme entre ces deux aspects est particulièrement sensible
pour les algorithmes de calcul formel, dont la correction repose habituellement
sur des concepts mathématiques élaborés, mais dont l’efficacité pratique
est une préoccupation importante.
Cette thèse développe des approches à l’étude formelle et l’exécution efficace
de programmes en théorie des types, et plus précisément dans l’assistant à la
preuve Coq. Dans un premier temps, nous présentons un environnement
d’exécution permettant de compiler en code natif de tels programmes tout
en conservant la généralité et l’expressivité du formalisme.
Puis, nous nous intéressons aux représentations de données et plus
particulièrement au lien formellement vérifié et automatisé entre représentations
adaptées aux preuves ou au calcul.
Ensuite, nous mettons à profit ces techniques pour l’étude d’algorithmes
en algèbre linéaire, comme le produit matriciel de Strassen, le procédé
d’élimination de Gauss ou la mise en forme canonique de matrices, dont
notamment la forme de Smith pour les matrices sur un anneau euclidien.
Enfin, nous ouvrons le champ des applications à la formalisation et au calcul
certifié des groupes d’homologie de complexes simpliciaux issus d’images
numériques.
Aug 06 2013
Séminaire Marelle : Sur la théorie des types homotopiques
Mardi 06/08/2013, à partir de 14h30, en salle Byron Blanc.
Orateur : Florent Brehard.
Titre : Sur la théorie des types homotopiques.
Résumé :
L’exposé aura une première partie sur les principes de bases des types d’homotopie.
La deuxième partie parlera plus précisément des sphères en dimension n.
Jul 17 2013
Séminaire Marelle : Automatisation de preuves en Coq par traduction en logique du premier ordre
Mercredi 17/07/2013, à partir de 10h30, en salle Byron Blanc.
Orateur : Antoine Grospellier.
Titre : Automatisation de preuves en coq par traduction en logique du premier ordre.
Résumé :
J’ai essayé de comprendre le fonctionnement des logiciels why (et sa tactique coq) et isabelle (principalement sa fonction sledgehammer). Maintenant je tente de modifier why pour prouver un maximum de lemmes de la bibliothèque de ssreflect automatiquement.
Jul 08 2013
Séminaire Marelle : Le théorème des trois cercles
Lundi 08/07/2013, à partir de 14h30, en salle Byron Blanc.
Oratrice : Julianna Zsido.
Titre : Le théorème des trois cercles.
Abstract:
The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certain area of the complex plane delimited by straight lines. After applying a transformation involving inversion this area is mapped to an area delimited by circles. We provide a formalisation of this rather geometric proof in Ssreflect, allowing us to formalise the proof from an algebraic point of view.
Jun 11 2013
Séminaire Marelle : Vérification formelle de certificats fondés sur le lemme de Hensel
Mardi 11/06/2013, à partir de 10h15, en salle Byron Blanc.
Orateur : Érik Martin-Dorel.
Titre : Vérification formelle de certificats fondés sur le lemme de Hensel.
Résumé :
Dans cet exposé, je présenterai les travaux effectués dans le cadre du projet TaMaDi visant à certifier formellement les résultats des algorithmes conçus pour trouver les pires cas pour l’arrondi correct des fonctions mathématiques. Les calculs menant à ces pires cas sont très longs (plusieurs années⋅CPU) et sont effectués en utilisant des programmes largement optimisés qui implantent des algorithmes très complexes. D’où l’intérêt d’utiliser un outil formel d’aide à la preuve tel que le logiciel COQ, afin de garantir formellement la correction de ces données numériques.Dans ce travail, nous nous intéressons en particulier à l’algorithme Stehlé-Lefèvre-Zimmermann, qui consiste en une phase de découpage du domaine et d’approximation polynomiale, suivie de la résolution de myriades d’instances du problème ISValP (Integer Small Value Problem), qui revient grosso modo à trouver toutes les petites valeurs d’un polynôme à coefficients entiers, modulo un grand entier. La dernière étape de ces calculs s’appuie notamment sur la version bivariée du lemme de Hensel.
Le lemme de Hensel est un outil clé en calcul formel qui, étant donné un polynôme sur les entiers et une racine modulo un nombre premier p, construit itérativement des racines modulo p2k, sous des hypothèses faciles à vérifier. La force du lemme de Hensel réside notamment en la présence d’une assertion d’existence (il existe un relèvement) et d’unicité (ce relèvement est unique). Nous avons formalisé ce dernier résultat (dans les cas univarié ainsi que bivarié) au sein d’une bibliothèque pour l’assistant de preuves COQ.
En s’appuyant sur ces preuves formelles, nous avons conçu puis formellement prouvé un vérificateur de certificats pour le problème ISValP. Nous avons également rendu effectif ce vérificateur de certificats, dont je présenterai plusieurs benchmarks.
