Séminaires SIESTE 2012/2013

Voici les résumés des séminaires SIESTE 2012/2013:

9 octobre 2012. Damien Stehlé. Manipuler les réseaux euclidiens. slides

Résumé: Un réseau est l’ensemble des combinaisons linéaires entières de vecteurs linéairement indépendants. Visuellement, le réseau forme une grille infinie de points régulièrement espacés. Les réseaux ont de
nombreuses applications en informatique. Entre autres, ils
apparaissent fréquemment en calcul formel, par exemple pour factoriser
les polynômes à coefficients rationnels, et en cryptographie, aussi
bien pour cryptanalyser que pour concevoir des protocoles.
L’algorithme LLL, du nom de ses auteurs Arjen Lenstra, Hendriz Lenstra
et László Lovász, permet de calculer une bonne représentation, ou
base, d’un réseau donné. Cette représentation fournit de
l’information intrinsèque sur le réseau manipulé. De nombreuses
applications ont suivi la publication de l’algorithme LLL, et, du fait
de ce succès, plusieurs accélérations algorithmiques ont par la suite
été proposées. L’approche la plus efficace aujourd’hui repose, en
interne, sur des calculs flottants en faible précision, donnant lieu à
un algorithme hybride numérique-algébrique.
Dans cet exosé, après une introduction du domaine, je décrirai
l’algorithme LLL et le principe de l’accélération numérique-algébrique.

16 octobre 2012.Louis Esperet. Utiliser la compression d’entropie pour rendre constructives des preuves existentielles.

Résumé: Le Lemme Local de Lovász (l’autre LLL ndlr) est un outil puissant qui permet de montrer
de manière très simple l’existence d’objets combinatoires avec
certaines propriétés. Il affirme que si un certain nombre
d’événements ont tous une petite probabilité et que ceux-ci ne sont
pas trop interdépendants, la probabilité qu’aucun événement n’arrive
est non nulle.
Le problème était (jusqu’à une date récente) que cet outil n’était pas
constructif. J’expliquerai les idées (très jolies et étonnamment
simples) basées sur la compression d’entropie qui ont permis à Robin Moser
d’obtenir une version algorithmique de ce lemme. Je donnerai deux
exemples :

1) Si on a une suite de listes L_1, L_2, L_3, … à quatre éléments on
peut trouver (efficacement) dans chaque liste L_i un élément a_i tel
que le mot a_1 a_2 a_3 … n’a pas de carré (i.e. de sous-mot de la
forme x1 x2 … x_k x_1 x_2 … x_k).

2) Toute instance de k-SAT dans laquelle chaque clause a des variables
en commun avec au plus 2^(k-2) autres clauses est satisfiable (et on
peut trouver une bonne assignation vrai/faux aux variables de manière
efficace).

27 novembre 2012.Manuel Bodirsky. A Short Introduction to Constraint Satisfaction Problems.

Résumé: Many computational problems originating in various areas in theoretical computer science
can be formulated as constraint satisfaction problems (CSPs). In such problems,
we are given a finite set of variables and a finite set of constraints on those variables,
and the task is to find an assignment to the variables that satisfies all constraints.
Depending on the choice of the possible constraints, such problems might
be computationally hard, or feasible.
In recent years, a fascinating theory starts to emerge that provides strong
criteria implying hardness, or the existence of polynomial-time algorithms for such problems.
Questions that are motivated by this line of research are of central interest in finite model theory,
structural combinatorics, and universal algebra. I will give a short introduction to current
research on CSPs that directly leads to some of the outstanding open questions of the field.

4 décembre 2012.Jade Alglave. Reasoning about Weak Memory.

Résumé: Multiprocessors are now prominent, but provide execution models that are quite
subtle. To write correct concurrent programs, we need formal models describing
the behaviours that a multiprocessor allows or not. In this talk, I will
present a class of relaxed memory models, defined in the Coq proof assistant,
parameterised by the chosen permitted local reorderings of reads and writes,
and the visibility of inter- and intra-processor communications through memory
(e.g. store atomicity relaxation). We prove results on the required behaviour
and placement of memory fences to restore a given model (such as Sequential
Consistency) from a weaker one. Based on this class of models we develop a
tool, diy, that systematically and automatically generates and runs litmus
tests to determine properties of processor implementations. We detail the
results of our experiments on Power and the model we base on them. This work
identified a rare implementation error in Power 5 memory barriers.