Catégorie : Séminaires

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 p^2k, 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.

Désolé, cet article est seulement disponible en Anglais Américain.

Mardi 19/03/2013, à partir de 14h, en salle Byron Blanc.

Orateur : José Grimm.

Titre : Ordinaux et récursivité.

Résumé :
Dans la théorie des ensembles de Zermelo Fraenkel on peut définir un type particulier d’ensembles, les ordinaux, avec des opérations (somme, produit, puissance), et une relation d’ordre compatible avec les opérations. Les ordinaux généralisent les entiers naturels. Beaucoup de preuves se font par induction transfinie (une variante de l’induction sur les entiers). Il y a beaucoup trop d’ordinaux pour en faire un ensemble (ou un type Coq). On peut définir (par induction transfinie) des suites d’ordinaux epsilon(x), Gamma(x), etc. Si E est l’ensemble des ordinaux plus petits que epsilon(0) ou Gamma(0), E est stable par addition, multiplication, exponentiation, et est dénombrable. On peut le définir dans Coq comme un sous-type inductif via un constructeur constant zero, et un autre de type E→nat→E→E ou E→E→nat→E→E. Je montrerai le lien entre mon implémentation des ordinaux de Bourbaki, et les travaux de Pierre Castéran.

Lundi 18/02/2013, à partir de 15h30, en salle Byron Blanc.

Orateur : Érik Martin-Dorel.

Titre : Du lemme de Hensel aux certificats ISValP.

Résumé :
Le lemme de Hensel est un outil clé en calcul formel qui, étant donné un polynôme sur les entiers et une racine modulo p, construit itérativement des racines modulo p^2k, 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 et d’unicité. Nous avons formalisé ce dernier résultat dans les cas univarié ainsi que bivarié au sein de la bibliothèque CoqHensel (en utilisant Ssreflect). Puis nous avons déduit de ce résultat la correction d’un vérificateur de certificats pour le problème des petites racines entières d’un polynôme (ou de deux polynômes bivariés). En s’appuyant sur ce vérificateur bivarié, nous avons alors formalisé un vérificateur pour le problème ISValP (Integer Small Value Problem), dont le but ultime est de certifier formellement les pires cas pour l’arrondi correct des fonctions élémentaires. Enfin, à l’aide du système de modules de Coq et des bibliothèques BigZ, Flocq et Coq.Interval, nous avons rendu effectifs ces vérificateurs de certificats, dont je présenterai quelques benchmarks.

Mardi 29/01/2013, à partir de 10h30, en salle Byron Blanc.

Orateur : Guillaume Cano.

Titre : Forme normale de Frobenius et de Jordan d’une matrice.

Résumé :
Nous verrons comment a été formalisé la notion de matrice diagonale par blocs. Nous verrons ensuite comment à partir de cette notion et de la forme normale de Smith nous obtenons les forme normales de Frobenius et de Jordan d’une matrice.

Jeudi 09/08/2012, à partir de 14h, en salle Byron Blanc.

Orateur : Thomas Williams.

Titre : Vérification automatique de propriétés de « differential privacy ».

Résumé :
On cherche à montrer que des programmes faisant intervenir des tirages aléatoires ne révèlent pas trop d’informations sur leur entrée : la distribution des valeurs de sortie varie peu quand l’entrée varie peu.

Désolé, cet article est seulement disponible en Anglais Américain.

Mardi 07/12/2010, à partir de 10h30, en salle Byron Blanc.

Orateur : Yves Bertot.

Titre : Induction et co-induction mêlées.

Résumé :
Plusieurs expériences montrent que les types de données qui mélangent de l’induction et de la co-induction peuvent être utiles pour la programmation. En particulier, cela permet de décrire la productivité de certains algorithmes qui ne respectent pas les conditions de garde du système Coq. Dans cet exposé, nous nous concentrerons sur une description particulière de la séquence de Fibonacci, qui est bien formée du point de vue sémantique, mais qui est rejetée par la condition de garde. Nous montrerons comment cette description peut être modélisée en combinant de la co-récursion acceptée par Coq et de la récursion relative à un prédicat inductif.

Mardi 30/11/2010, à partir de 11h, en salle Byron Beige.

Orateur : Loïc Pottier.

Titre : L’axiome d’univalence de Voevodsky et l’extensionnalité.

Lien : http://docs.google.com/View?id=dgdtwh98_10964bjch4j

Mardi 16/11/2010, à partir de 11h, en salle Euler Bleu.

Oratrice : Ioana Pasca.

Titre : Vérification formelle pour les méthodes numériques.

Résumé :
Répétition de la thèse de doctorat.