### Next talk

Special talks

Wednesday April 24, 2019, 9AM, Amphitheater Turing

**Laurent Viennot, Guillaume Chapuy, Claire Mathieu, Ahmed Bouajjani, Amaury Pouly, Constantin Enea, Yves Guiraud, Jean Krivine, Hugo Herbelin** (IRIF) *Scientific talk series for the visit of Ali Charara, head of INS2I at CNRS*

### Previous talks

#### Year 2019

Special talks

Wednesday April 17, 2019, 7PM, 3052

**Thatchaphol Saranurak** (Toyota Technological Institute at Chicago) *Breaking Quadratic Time for Small Vertex Connectivity (live video projection of TCS+ talk)*

In this talk, I will present a randomized Monte Carlo algorithm with ~O(m + k^3 n) time. This algorithm proves the conjecture by Aho, Hopcroft, and Ullman when k=O(1) up to a polylog factor, breaks the 50-year-old bound by Kleitman, is fastest for 4 < k < n^{0.456}. The story is similar for the directed graphs where we obtain an algorithm running time at most ~O(k^2 m).

The key to our results is to avoid computing single-source connectivity, which was needed by all previous exact algorithms and is not known to admit o(n^2) time. Instead, we design the first local algorithm for computing vertex connectivity; without reading the whole graph, our algorithm can find a separator of size at most k or certify that there is no separator of size at most k “near” a given seed node.

This talk is based on joint works with Danupon Nanongkai and Sorrachai Yingchareonthawornchai.

Special talks

Wednesday April 10, 2019, 2PM, Salle 3058

**Lélia Blin** (LIP6) *Algorithmes auto-stabilisants*

Special talks

Thursday April 4, 2019, 1PM, Salle 3052

**Kais Klai** (LIPN) *Model Checking of Stuttering-Invariant Temporal Properties Using Hybrid Graphs*

Special talks

Wednesday April 3, 2019, 1PM, Salle 1007

**Josef Widder** (Technische Universitaet Wien (Vienne, Autriche)) *Distributed Algorithms meet Computer-Aided Verification*

The observation that distributed algorithm theory has interesting application in computer-aided verification motivated me to explore this connection in more depth. In the second part of the talk, I will present a line of research that in the recent years led to breakthroughs in parameterized model checking of fault-tolerant broadcasting algorithms. I will close the talk by discussing ongoing research lines and open challenges.

The results on link reversal is joint work with Bernadette Charron-Bost, Matthias Fuegger, Antoine Gaillard, and Jennifer Welch. Parameterized model checking of broadcasting algorithms is joint work with Igor Konnov, Marijana Lazic, and Helmut Veith.

Special talks

Friday March 29, 2019, 1PM, Salle 3052

**Duong-Hieu Phan** (XLIM, Université de Limoges) *Extractable Linearly-Homomorphic Signatures and Scalable Mix-Nets in Voting Schemes*

In this talk, we propose a new approach for proving correct shuffling based on the new notion of extractable linearly-homomorphic signature: the mix-servers can simply randomize individual ballots (meaning the ciphertexts, the signatures, and the verification keys) with an additional global proof of constant size, and the output will be publicly verifiable. The computational complexity for the mix-servers is linear in the number of ciphertexts. It also remains linear in the number of ciphertexts for the verifiers, independently of the number of rounds of mixing. This leads to the most efficient technique of mix-nets, which is at the same time highly scalable.

(Joint work with Hebant Chloé and David Pointcheval)

Special talks

Thursday March 28, 2019, 1PM, Salle 3052

**Anne Etien** (LIFL) *Code transformations: two cases*

Special talks

Tuesday March 26, 2019, 4PM, Salle 3052

**Marc Pouzet** (ENS Paris) *Zelus, un langage synchrone fonctionnel pour les systèmes hybrides*

Les langages synchrones décrivent des systèmes à temps discret seulement. Ils ne permettent pas de modéliser, ni fidèlement ni très efficacement des systèmes contenant des dynamiques hybrides combinant des signaux à temps discret et à temps continu. Cela créé une rupture dans la chaîne de développement, avec un langage pour la modélisation hybride et un autre pour la modélisation ou l'implémementation du logiciel de contrôle.

Dans cet exposé, nous présenterons Zelus, une extension d'un langage synchrone avec des équations différentielles ordinaires (ODEs) et une opération de détection d'événement (zero-crossing). Il permet d'écrire dans un source unique, un modèle synchrone (à temps discret) du logiciel de controle et un modèle (à temps discret où à temps continu) de son environnement. Nous illustrerons le langage sur quelques exemples. Nous présenterons son système de types qui permet de cloisonner les parties à temps discret et les parties à temps continu pour rejeter des comportements étranges que l'on obtient avec les outils de modélisation hybrides les plus utilisés. Nous montrerons également son analyse par typage des boucles de causalité par typage. Enfin, nous montrerons le principe utilisé pour générer du code séquentiel qui est lié ensuite à un solveur numérique (ici Sundials Cvode). Si le temps le permet, nous discuterons une expérimentation en cours, d'ajout de contructions de programmes probabilistes, ainsi que quelques questions ouvertes autour du typage, de la sémantique et de la vérification.

Special talks

Thursday March 21, 2019, 1PM, Salle 3052

**Reem Yassawi** (Université de Lyon) *Les automates cellulaires et dynamique symbolique*

Le premier problème concerne les propriétés de randomisation de certains automates cellulaires. La randomisation asymptotique est le processus par lequel un état initial de basse entropie est asymptotiquement transformée en un état d'entropie maximale, par l’action itérée de l’automate cellulaire. Je discute des conditions nécessaires et suffisantes pour qu’une telle randomisation survienne, et aussi d'un travail récent avec Eric Rowland.

La deuxième problématique est de caractériser les automates cellulaires qui préservent un langage donné. Je résume un travail récent avec Clemens Muellner, où nous obtenons un théorème de structure pour les automates cellulaires qui préservent certains langages HD0L.

Special talks

Wednesday March 20, 2019, 1PM, Salle 3052

**Lin Chen** (LRI) *Algorithm Design and Analysis in Wireless Networks*

Special talks

Thursday February 21, 2019, 2PM, Salle 3052

**Pablo Arrighi** (Aix-Marseille Université) *Quantum, automata, computability and universality*

Special talks

Thursday February 21, 2019, 11:45AM, Salle 1007

**Samuele Giraudo** (Université Paris-Est Marne-la-Vallée) *Graded graphs and operads*

Special talks

Wednesday February 20, 2019, 1PM, Salle 3052

**Giulio Manzonetto** (LIPN) *A syntactic and semantic analysis of program equivalences*

Special talks

Thursday February 7, 2019, 1PM, Salle 3052

**Sylvain Schmitz** (LSV) *The complexity of reachability in vector addition systems*

In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, a landmark result in theoretical computer science, with applications in an array of fields ranging from program verification to data logics. The decidability of the problem was first shown by Mayr thanks to a decomposition algorithm. I will present succinctly the main ideas behind a tight Ackermannian complexity upper bound obtained with Jérôme Leroux for this algorithm.

#### Year 2018

Special talks

Thursday September 20, 2018, 10:30AM, Amphi Turing (bâtiment Sophie Germain)

**Leonid Libkin** (University of Edinburgh) *Certain Answers Meet Zero-One Laws*

This measure is defined as the probability that the query is true under a random interpretation of missing information in a database. Since there are infinitely many such interpretations, to pick one at random we adopt the approach used in the study of asymptotic properties and 0-1 laws for logical sentences and define the measure as the limit of a sequence. We show that in the standard model of missing data, the 0-1 law is observed: this limit always exists and can be only 0 or 1 for a very large class of queries. Thus, query answers are either almost certainly true, or almost certainly false, and this classification behaves very well computationally. When databases satisfy constraints, the measure is defined as the conditional probability of the query being true if the constraints are true. This can now be an arbitrary rational number, which is always computable. Another refinement of the notion of certainty views answers with a larger set of interpretations that make them true as better ones. We pinpoint the exact complexity of finding best answers for first-order queries.

Special talks

Thursday July 5, 2018, 2PM, Salle 3052

**Laurent Viennot** (Inria Paris et IRIF) *Introduction to the blockchain*

Special talks

Tuesday February 20, 2018, 2PM, 3052

**Daniela Petrisan** (IRIF) *Up-To Techniques for Behavioural Metrics via Fibrations*

behavioural equivalences between systems. In this talk, I introduce up-to techniques for behavioural metrics in a coalgebraic setting and provide general results that show under which conditions such up-to techniques are sound.

For a system modelled as a coalgebra for a certain functor, the behavioural distance can be seen as a coinductive predicate using a suitable lifting of the functor. I will focus on the so called Wasserstein lifting of a functor for which we provide a new characterization in a fibrational setting. This is useful for automatically proving the soundness of up-to techniques via a generic framework developed in a previous CSL-LICS'14 paper.

I will use fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our framework I provide an example on distances between regular languages.

Special talks

Thursday February 1, 2018, 2PM, 3052

**Vincent Danos** (ENS) *Contractivity of Markov chains (metric couplings)*

Special talks

Tuesday January 30, 2018, 2PM, 3052

**Vincent Danos** (ENS) *Bayesian inversion and approximation*

Special talks

Thursday January 25, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Quantitative equational logic and free Kantorovich algebras*

Special talks

Tuesday January 23, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Metrics for LMPs*

Special talks

Thursday January 18, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *A dual point of view: LMPs as function transformers*

Special talks

Tuesday January 16, 2018, 2PM, 3052

**Prakash Panangaden** (McGill University) *Introduction to LMPs: bisimulation, simulation, logical characterization*