29 janvier 2013.Pascal Cuoq. Collaboration d’analyses dans Frama-C.

Résumé: Frama-C est une plateforme collaborative d’analyse statique pour le langage C. Chaque technique ou idée peut être implémentée dans Frama-C sous la forme d’un greffon.

Un moyen de collaboration entre greffons est par le langage de spécification ACSL : l’analyse de valeurs, un greffon d’interprétation abstraite, insère dans le programme cible des assertions ACSL pour chaque comportement non défini qu’elle est incapable d’exclure. Ces assertions peuvent être vérifiées par un autre greffon, tel qu’un greffon basé sur la logique de Hoare.

12 février 2013.Clément Pernet. Calcul de formes normales matricielles: de l’algorithmique à la mise en pratique. slides

Résumé: En algèbre linéaire, les formes normales fournissent des représentants uniques pour les classes d’équivalence selon différentes transformations: la forme normale de Frobenius pour la similitude dans un corps, la forme normale de Hermite pour l’équivalence dans un anneau ou de Gauss-Jordan pour l’équivalence dans un corps.
Leur calcul permet en outre de révéler la plupart des caractéristiques d’une matrice, comme le rang, le profil de rang, le déterminant, les facteurs invariants, etc.
De nombreux progrès ont été réalisé au cours des 20 dernières années concernant d’une part la réduction des complexités des algorithmes, et d’autre part les techniques logicielles pour des implantations efficaces.
Nous présenterons une sélection de ces techniques algorithmiques et logicielles appliquées à l’élimination de Gauss, le calcul de la forme normale de Frobenius et de la forme normale de Hermite.

19 février 2013.Corinne Touati. Quelques conséquences contre-intuitives d’une prise de décision distribuée.

Résumé: La théorie de la décision rationnelle, et plus particulièrement sa composante distribuée, la théorie des jeux, a connu un fort développement depuis la formalisation de la notion d’équilibre par Nash dans les années 50. Ses applications en économie ont été récompensées par pas moins de 12 prix Nobel depuis les années 90. Le dernier en date (novembre 2012) a été attribué à Lloyd Shapley et Alvin Roth notamment pour leurs applications au partage de ressources.
Nous allons justement dans cet exposé regarder quelques (contre-) exemples du lien entre optimisation distribuée et prise de décision (optimale) distribuée dans des problèmes d’allocation de ressources tirées d’exemples de réseaux de communications.

19 mars 2013.Claire Mathieu. Algorithms for Optimization over Noisy Data.

Résumé: To deal with NP-hard reconstruction problems, one natural possibility consists in assuming that the input data is a noisy version of some unknown ground truth. We present several examples, in particular correlation clustering, and transitive tournaments. In correlation clustering, the goal is to partition data given pairwise similarity and dissimilarity information, and sometimes semi-definite programming can, with high probability, reconstruct the optimal (maximum likelihood) underlying clustering. The proof uses semi-definite programming duality and the properties of eigenvalues of random matrices. The transitive tournament problem asks to reverse the fewest edge orientations to make an input tournament transitive. In the noisy setting it is possible to reconstruct the underlying ordering with high probability using simple dynamic programming.

26 mars 2013.Jean-Sébastien Sereni. Limites de graphes denses.

Résumé: Le but de cet exposé est de fournir une introduction à la théorie des limites
de graphes denses, développée depuis 2005 principalement par Lovász et ses
co-auteurs. Outre une introduction générale aux fondements de la théorie, un
exemple concret d’application à un problème extrémal sera détaillé.

2 avril 2013.David Coeurjolly. Introduction à la géométrie discrète et axe médian discret minimal. slides

Résumé: L’objectif de la présentation sera de faire une petite introduction à la géométrie discrète et de se focaliser sur un problème combinatoire particulier : le calcul d’un axe médian discret minimal. Il s’agit de construire une représentation d’un objet discret (partie de Z^n) comme union d’un ensemble de boules discrètes (discrétisation boule euclidienne), si possible de cardinalité minimale. Ce problème a l’avantage d’être auto-suffisant et simple à décrire mais nous emmènera vers une preuve de NP-complétude « géométrique » assez amusante (bon… à minima intéressante…).

9 avril 2013.Tom Hirschowitz. Vers une théorie des langages de programmation. slides

Résumé: On sait de mieux en mieux raisonner sur les langages de programmation,
comme en témoignent, par exemple, les récents progrès en matière de
certification de compilateurs. En revanche, même si on a des méthodes,
qu’on peut reproduire, on sait mal pour l’instant formaliser des
résultats généraux, pouvant s’appliquer à plusieurs langages.
L’exposé abordera quelques approches envisagées pour remédier à cette
situation. A l’instar, quelques années plus tôt, des mathématiciens
ayant défini des notions générales de groupe, anneau, etc, toutes ces
approches tentent de dégager une notion générale de langage de
programmation.

16 avril 2013.Samuel Hym. Evaluation de la consommation mémoire de programme.

Résumé: Pour éviter qu’un logiciel (en particulier dans des systèmes critiques) ne fasse d’erreurs par manque de mémoire, on veut borner la quantité de mémoire qu’il peut nécessiter. Dans de nombreux langages (tels que Java, Ocaml ou encore Javascript) les désallocations ne sont pas gérées explicitement par le programmeur: le garbage collector (GC) s’y charge d’identifier les objets morts et de récupérer leur mémoire. On verra donc dans cet exposé quelques unes des difficultés à résoudre pour obtenir un résultat suffisamment proche de la réalité. Quels problèmes engendrent exactement les GCs? Comment décomposer le problème pour arriver à traiter des programmes qui ne soient pas juste jouets? Comment traiter les nids de boucle?