Institut de recherche mathématique avancée

Résumé : Formal Verification enables one to prove that a program does not contain any bug. In this talk, I will present state-of-the-art techniques for formally verifying the implementation of a nontrivial algorithm or data structure. First, I will explain how to formulate as a mathematical theorem a statement of the form: "this program behaves as intended". Second, I will explain how to leverage an "interactive proof assistant", a tool for developing machine-checked mathematical proofs, for reasoning about the behavior of the source code of the program. Finally, I will give a survey of complex programs that have been formally verified in the past decade, assessing the progress made since the pioneering work by Hoare-Floyd-Dijkstra in the late 60's.

The seminar will be also broadcasted via BBB: https://bbb.unistra.fr/b/hum-51d-suf-mzq

Arthur Charguéraud is an Inria researcher, member of the ICube lab since 2016. He completed his PhD in 2010 at Inria Paris-Rocquencourt, then spent 18 months as a post-doc at the Max Plank Institute for Software Systems in Kaiserslautern. He was recruited at Inria Saclay in 2012, then moved to Strasbourg in 2016. His research is focused on program verification and program optimization.

Résumé : A celebrated part in the classification of Fano threefold is Mukai's vector bundle method. One of the main result is an existence (and rigidity) result for vector bundles with rank dividing the genus, for prime Fano threefolds of index 1. Unfortunately, in the literature, the proof has a gap. I will present joint work with Arend Bayer and Alexander Kuznetsov, where we fill this gap.

Résumé : L'échantillon de n variables aléatoires réelles indépendantes et identiquement distribuées est l'objet d'étude le plus basique des statistiques. Le comportement de la somme d'un tel échantillon (sous l'hypothèse d'une variance finie) est bien connu : c'est le Théorème Central Limite (TCL). Comme son nom l'indique, ce théorème nous renseigne sur la partie "centrale" de la distribution (là où le poids de probabilité est concentré). Si au contraire nous voulons nous intéresser à la queue droite (resp. gauche) de la distribution, la variable d'intérêt sera le maximum (resp. le minimum) de l'échantillon. À l'instar de la somme, le comportement du maximum est aussi connu : c'est le Théorème des Valeurs Extrêmes (TVE). L'objectif de ce séminaire est d'explorer l'analogie entre ces deux théorèmes fondamentaux.

Résumé : A hyper-Kähler manifold is a complex Kähler manifold that is simply connected, compact, and has a unique holomorphic symplectic form, up to constants.
This important class of manifolds has been studied in the past in many contexts, from an arithmetic, algebraic, geometric point of view, and in applications to physics and dynamics.

The theory in dimension two, namely K3 surfaces, is well understood.
The aim of the seminar is to give an introduction to the theory of hyper-Kähler manifolds in higher dimension, from a point of view of their classification; in particular, about existence of Lagrangian fibrations.
We will present some results in dimension four, obtained in collaboration with Olivier Debarre, Daniel Huybrechts and Claire Voisin.

Résumé : En 2000, Eliashberg et Polterovich introduisirent la notion d'ordonnabilité pour étudier la structure des groupes de contactomorphismes et des classes d'isotopie de sous-variétés legendriennes. En peu de mots, le groupe des contactomorphismes est ordonnable si la relation binaire sur les flots de contact au temps 1 naturellement induite par l'ordre partiel sur leurs hamiltoniens est elle-même un ordre partiel. Au cours des deux dernières décennies, ordonnabilité et non-ordonnabilité ont été principalement étudiées au moyen de selecteurs spectraux basés sur des théories dérivées de celle de Floer et sur les fonctions génératrices. Dans cet exposé, nous expliquerons en quoi l'ordonnabilité est équivalente à l'existence de sélecteurs spectraux et en donnerons quelques applications.