Exposés (45mn)
Patrick Baillot
(LIP, Lyon)Titre: Implicit Computational Complexity of Subrecursive Functional Programs, with Applications to Cryptographic Proofs.
Résumé: We address the problem of automatically analysing the complexity of higher-order functional programs with imperative features. Our motivation is to provide analysis techniques that could be employed for cryptographic reduction proofs. For that we consider as source language a typed lambda-calculus with references and structural recursion. Our analysis employs a type system which tracks the sizes of values by means of parameterized types, using some linearity ideas. We present its main properties and discuss open questions. We illustrate the expressivity of this approach with the example of the construction of adversary in the Goldreich-Levin theorem on hardcore predicates. (joint work with Gilles Barthe and Ugo Dal Lago)
Nicolas Bonichon
(LABRI, Bordeaux)Titre: Quelques résultats sur les spanners géométriques.
Résumé: Un graphe géométrique est un graphe défini à partir d'un nuage de points (par exemple dans le plan). L'étirement d'un graphe géométrique est le pire rapport entre la distance dans le graphe et la distance Euclidienne, pour toute paire de points du graphe. Un t-spanner est un graphe (ou une famille de graphes) dont l'étirement est borné par t. Dans cet exposé je présenterai quelques résultats relatifs à certains spanners : triangulations de Delaunay, Theta-graphs, spanners de degré borné,...
Pierre Calka
(LMRS, Rouen)Titre: Enveloppe convexe de points aléatoires.
Résumé: Nous considérons un nuage aléatoire de points de Rd indépendants et de même loi et nous construisons son enveloppe convexe. Notre but est de décrire le comportement asymptotique du polytope aléatoire obtenu lorsque la taille du nuage tend vers l'infini. En particulier, nous nous intéressons d'une part à certaines variables aléatoires telles que le nombre de points extrémaux, le nombre de faces de dimension fixée ou le volume et d'autre part à des limites d'échelle de la frontière de l'enveloppe convexe. Les premiers résultats sur le sujet remontent aux articles fondateurs de A. Rényi et R. Sulanke en 1963 et 1964 et concernent des calculs asymptotiques de moyennes dans le cas où les points sont uniformes dans un corps convexe fixé ou sont de loi gaussienne. Nous proposons dans cet exposé une méthode inédite qui fournit la convergence du processus frontière du polytope et le calcul explicite de variances limites. Celle-ci repose sur la notion de stabilisation pour des processus ponctuels de Poisson et l'utilisation de graphes de dépendance. Nous discuterons en détail le cas de points uniformes dans un polytope simple fixé. Cet exposé est issu de plusieurs travaux en collaboration avec T. Schreiber et J. Yukich.
Alain Couvreur
(LIX, Saclay)Titre: Cryptographie basée sur les codes correcteurs.
Résumé: Initialement les codes correcteurs d'erreurs étaient utilisés afin de "réparer" un message qui aurait été transmis via un canal bruité. Cependant, à la fin des années 70, R.J. McEliece propose d'utiliser des codes correcteurs d'erreurs pour faire de la cryptographie à clé publique. Bien que peu utilisé en pratique, le schéma de chiffrement de McEliece bénéficie d'un regain d'intérêt ces dernières années. Ce succès vient entre autres du fait que, à la différence des systèmes de chiffrement classiquement utilisés comme par exemple RSA, le schéma de McEliece résisterait à l'ordinateur quantique. Dans cet exposé, nous présenterons ce système, ses avantages et inconvénients, ainsi que les récentes avancées dans ce domaine.
Delphine Demange
(IRISA, Rennes)Titre: Mechanized Verification of SSA-based Compilers Techniques.
Résumé: Modern optimizing compilers rely on the Static Single Assignment (SSA) form to make optimizations fast and simpler to implement. In this talk, I will recall the basics of SSA, and discuss the challenges that it raises in the context of verified compilation. Then, I will report on our results obtained so far within the CompCertSSA project, which extends the CompCert compiler with an SSA middle-end.
Christian Gentil
(Le2I, Dijon)Titre: Les objets fractales : de la conception à la fabrication.
Résumé: Les formes fractales possèdent des propriétés spécifiques : surfaces infinies, structures « volumiques » de mesure nulle. Ces propriétés présentent un intérêt pour l'industrie comme par exemple pour la conception d'échangeurs thermiques ou la conception d'objets allé gés. Les évolutions des procédés de fabrication additive rendent possible la matérialisation de ces formes et offrent l'opportunité de développer de nombreuses d'applications.
Cependant, la description et la conception de ces formes complexes sont peu aisées et peu intuitives de par les concepts sous-jacents auxquels les concepteurs ne sont pas habitués. À cela s'ajoute la difficulté de contrôler la topologie « non standard » et la géométrie de ces formes. Enfin, pour pouvoir fabriquer ces formes définies théoriquement comme limite d'une suite infinie d'opération de construction, il faut être capable de fournir une approximation définissant un volume cohérent pour pouvoir être interprété par les logiciels d'imprimante 3D.
Nous présentons le modèle BCIF S (Boundary Controlled Iterated Function System), dont le principe est de décrire la subdivision topologique des formes et de rendre indépendant le contrôle de la topologie et de la géométrie. Les formes géométriques sont décrites dans des espaces barycentriques et peuvent être modifiées dans l'espace de modélisation à l'aide de points de contrôle. Ce modèle englobe les NURBS et les surfaces de subdivisions. Nous avons développé un modeleur géométrique pour la conception et la fabrication de prototypes. Nous aborderons également l'étude des propriétés différentielles et l'évaluation d'opérateurs de CAO sur ces structures fractales.
Emmanuel Jeandel
(LORIA, Nancy)Titre: An aperiodic tiling using only 11 different Wang tiles.
Résumé: Wang tiles, introduced in the sixties by Hao Wang, are square tiles with colored edges. Given a finite set of tiles, where each can be used as many times as necessary, we are interested in tiling the discrete plane, i.e. putting a tile in each cell of the grid so that adjacent tiles match. Of particular interest are aperiodic tile sets, for which it is possible to tile the plane, but it is not possible to do it periodically. Aperiodic tile sets are the key ingredient in almost all results in tiling theory and multidimensional symbolic dynamics. Since the creation (or the discovery ?) of the first aperiodic tile set of 20426 tiles by Berger, a large number of aperiodic tile sets have been proposed during the years, culminating with a set of only 13 tiles found by Culik in 1996 using a method of Kari. With the help of a computer search, we were able to find an aperiodic set of 11 tiles, and prove that this number is optimal: no set of less than 11 Wang tiles is aperiodic. The result is quite different from traditional computer-aided searches, as we are actually looking for a needle in a uncomputable haystack: there is no algorithm able to decide, given as input a set of tiles, whether it is aperiodic. After an introduction to the problem, we will present our set of 11 tiles, along with techniques coming from automata theory and abstract rewriting systems we used to prove it is indeed an aperiodic set, and the smallest one.
Elham Kashefi
(LTCI, Paris)Titre: Quantum Verification.
Résumé: Quantum computing has an acute verification problem. Since classical computations cannot scale up to the computational power of quantum mechanics (QM), how can we hope to verify the result of a QM-mediated computation? The approaches that have been so far successful are those based on interactive proof systems, where a trusted, computationally limited verifier exchanges messages with an untrusted, powerful quantum prover(s). The verfifier attempts to certify that, with high probability, the prover are performing the correct quantum operations by encrypting simple tests to which one knows the answer within a computation. However the real challenge in adapting and combining these generic solutions to the specific architectures, is how to respect the criteria of a specific, and sometimes even a restricted, model. This will lead to a spectrum of various verification protocols depending on the criteria of the desired security, adversarial model, and verifier?s quantum and classical capacity that we will briefly summarise.
Christophe Negre
(DALI LIRMM, Perpignan)Titre: Approaches for RSA and (Hyper)elliptic Curve Cryptosystems Resistant to Simple Power Analysis.
Résumé: Some public key cryptosystems can be threaten by side channel analysis when they are implemented on an embedded device. For example in RSA cryptosystem, by measuring several computation times of a modular exponentiation and exploiting the difference of squaring and multiplication times, an attacker can recover part of the key. An attacker can also monitor the power consumption and then read the sequence of operations on the power trace and recover the key bits: this is the Simple Power Analysis (SPA). The basic approach to render an exponentiation immune to SPA analysis consists to have a sequence of operation uncorrelated to the secret key. In this talk we will present some recent improvements on such regular exponentiation for RSA and scalar multiplication on (hyper)elliptic curve.
Viviane Pons
(LRI, Orsay)Titre: Des relations binaires au treillis de Tamari.
Résumé: Nous définissons un certain treillis sur les relations binaires que l'on peut considérer comme une généralisation de l'ordre faible sur les permutations. De là, par des opérations de surjections et quotients, nous retrouvons de nombreux treillis liés à la combinatoire de l'ordre faible et du treillis de Tamari. La motivation de ce travail est l'étude de ces treillis qui s'interprètent souvent à la fois comme des algèbres de Hopf et des polytopes.
Adrien Richard
(I3S, Nice)Titre: Points fixes et cycles de rétroaction dans les réseaux booléens.
Résumé: Les réseaux booléens sont des systèmes dynamiques discrets qui se composent d'un nombre fini de variables binaires évoluant selon une lois prédéfinie. Ils ont de nombreuses applications, notamment dans le domaine de la modélisation des réseaux de gènes. Dans ce contexte, le premières informations fiables sont souvent représentées sous la forme d'un graphe d'interaction. Il est donc intéressant d'identifier les propriétés dynamiques d'un réseau booléen qui peuvent se déduire à la seule vue de son graphe d'interaction. Je présenterais des réponses partielles à ce problème, en mettant l'accent sur le nombre maximum de points fixes qu'un réseau booléen peut admettre en fonction de la structure des cycles de son graphe d'interaction.
Hélène Touzet
(CRISTAL, Lille)Titre: Algorithmique des structures d'ARN.
Résumé: L'ARN (Acide RiboNucléique) est l'un des trois grands types de molécules essentiels à la vie, avec l'ADN et les protéines. Il joue un rôle majeur au sein de la cellule dans la régulation de l'expression des gènes. Comme l'ADN, l'ARN est une chaîne de nucléotides. Une différence est que c'est une molécule simple brin, qui adopte une structure tri-dimensionnelle construite sur la base d'appariements deux à deux. De ce fait, les molécules d'ARN sont modélisées par des modèles combinatoires discrets tels que les arbres ordonnés ou les graphes. Dans cet exposé, je présenterai les problèmes classiques posés par l'analyse de structures d'ARN (inférence de structure, comparaison), ainsi qu'un cadre universel pour la conception d'algorithmes de programmation dynamique, qui est particulièrement bien adapté à l'analyse de structures d'ARN.