## Welcome to IRIF

IRIF is a research laboratory of CNRS and Université Paris-Diderot, also hosting two INRIA project-teams.

The scientific objectives of IRIF are at the core of computer science and, in particular, they focus on the conception, analysis, proof, and verification of algorithms, programs, and programming languages. They are built upon fundamental research activities developed at IRIF on combinatorics, graphs, logics, automata, type, semantics, and algebras.

IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), and two of them are members of the Institut Universitaire de France (IUF).

## News

*08.03.2018*

In the scope of the IRIF Distinguished Talks Series
**Monika Henzinger** (University of Vienna) will give on **April 13** a talk on
*“The state of the art in dynamic graph algorithms”*.

*02.03.2018*

Adrian Kosowski (IRIF), together with Bartek Dudek (University of Wroclaw),
will present at STOC 2018 a new protocol for spreading information
in a population. This is the first time that methods of oscillatory dynamics
are used to solve a basic task of information dissemination.

*27.02.2018*

Constantin Enea (IRIF) is an organizer of the 2018 edition of the
EPIT **research school**, on the subject of software verification, to he held in Aussois on **May 7-11 2018**.

*27.02.2017*

FSMP offers **20 PhD student positions** in Maths and TCS under
H2020 COFUND project MathInParis. As a member of the FSMP network, IRIF is an eligible hosting lab.
Call for application is open until **April, 1st 2018**. Applicants must be international students, but master students already in France for less than a year are eligible.

*27.02.2018*

Peter Habermehl (IRIF) and Benedikt Bollig
(LSV, ENS Paris-Saclay) organize the **research school**
MOVEP (*Modelling and Verification of Parallel Processes*), from on **July 16-20** in Cachan.

*05.02.2017*

Université Paris Diderot has opened **three permanent positions** in
Computer Science
(1 professor on Graph and applications, 1 assistant professor on Software Science,
1 assistant professor on Data Science).
Recruited researchers will join IRIF.

*04.02.2017*

Laurent Viennot (IRIF, Inria) is Scientific Curator of the exhibition Informatique et sciences du numérique, at **Palais de la découverte**, starting **March 13, 2018**.

*02.02.2017*

Amina Doumane, now at LIP, was awarded the **“La Recherche” prize** in the Computer Science category for her paper
entitled Constructive Completeness for the linear-time mu-calculus,
a work accomplished during her PhD at IRIF and that appeared in the proceedings of LICS’17.

*01.02.2017*

The first **on-the-fly quantum money transaction** was implemented by researchers in Paris,
including Iordanis Kerenidis. Quantum money is provably unforgeable due to the no-cloning property of quantum information.

## Events

Théorie des types et réalisabilité

lundi 19 mars 2018, 13h15, 3052

**Adrien Guatto** () *A Generalized Modality for Recursion*

Nakano’s later modality allows types to express that the output of a function does not immediately depend on its input, and thus that computing its fixpoint is safe. This idea, guarded recursion, has proved useful in various contexts, from functional programming with infnite data structures to formulations of step-indexing internal to type theory. Categorical models have revealed that the later modality corresponds in essence to a simple reindexing of the discrete time scale.

Unfortunately, existing guarded type theories suffer from significant limitations for programming purposes. These limitations stem from the fact that the later modality is not expressive enough to capture precise input-output dependencies of functions. As a consequence, guarded type theories reject many productive definitions. Combining insights from guarded type theories and synchronous programming languages, we propose a new modality for guarded recursion. This modality can apply any well-behaved reindexing of the time scale to a type. We call such reindexings time warps. Several modalities from the literature, including later, correspond to fixed time warps, and thus arise as special cases of ours.

We integrate our modality into a typed λ-calculus. We equip this calculus with an operational semantics, as well as an adequate denotational semantics in the topos of trees, a standard categorical model for guarded recursion. Building on top of categorical ideas, we describe an abstract type-checking algorithm whose completeness entails the coherence of both semantics.

Vérification

lundi 19 mars 2018, 11h00, Salle 1007

**Rupak Majumdar** (MPI-SWS, Germany) *Effective Random Testing for Concurrent and Distributed Programs*

Random testing has proven to be an effective way to catch bugs in distributed systems. This is surprising, as the space of executions is enormous. We provide a theoretical justification of the effectiveness of random testing under various “small depth” hypotheses. First, we show a general construction, using the probabilistic method from combinatorics, that shows that whenever a random test covers a fixed coverage goal with sufficiently high probability, a small randomly-chosen set of tests achieves full coverage with high probability. In particular, we show that our construction can give test sets exponentially smaller than systematic enumeration. Second, based on an empirical study of many bugs found by random testing in production distributed systems, we introduce notions of test coverage which capture the “small depth” hypothesis and are empirically effective in finding bugs. Finally, we show using combinatorial arguments that for these notions of test coverage we introduce, we can find a lower bound on the probability that a random test covers a given goal. Our general construction then explains why random testing tools achieve good coverage—and hence, find bugs—quickly.

Systèmes complexes

mardi 20 mars 2018, 14h00, Salle 1007

**Tba** () *TBA*

TBA

Graphes

mardi 20 mars 2018, 14h00, Salle 1007

**Pierluigi Crescenzi** (Universite de Pise) *Computing node centrality in large graphs: from theory to practice and back*

The computation of several graph measures, based on the distance between nodes, is very often part of the analysis of real-world complex networks. The diameter, the betweenness and the closeness centrality, and the hyperbolicity are typical examples of such measures. In this talk, we will focus on the computation of one specific measure, that is, the node closeness centrality which is basically the inverse of the average distance of a node from all other nodes of the graph. Even though polynomial-time algorithms are available for the computation of this measure, in practice these algorithms are not useful, due to the huge size of the networks to be analysed. One first theoretical question is, hence, whether better algorithms can be designed, whose worst-case complexity is (almost) linear in the size of the input graph. We will first show that, unfortunately, for the closeness centrality no such algorithm exists (under reasonable complexity theory assumptions). This will lead us back to the practical point of view: we will then describe a heuristics that allows us to compute the above measure in (practical) linear time, even though its worst-case complexity is (in practice) intractable. This result will finally motivate our return to theory in order to understand the reason why, in practice, this heuristics works so well: we will indeed conclude by showing that, in the case of several random graph generating models, the average time complexity of the heuristics is indeed (almost) linear. This talk will summarise the research work that I have done in collaboration with Elisabetta Bergamini, Michele Borassi, Michel Habib, Andrea Marino, Henning Meyerhenke, and Luca Trevisan, and will be mostly based on two papers presented at ALENEX 2016, and SODA 2017.

Algorithmes et complexité

mardi 20 mars 2018, 11h00, Salle 1007

**Valia Mitsou** (IRIF) *On the complexity of defective coloring.*

In defective coloring, we are given a graph G and two integers c, ∆* and are asked if we can c-color G so that the maximum degree induced by any color class is at most ∆*. This problem is a generalization of proper coloring, for which Δ* = 0.

Defective coloring, like proper coloring, has many applications, for example in scheduling (assign jobs to machines which can work on up to Δ* jobs in parallel), or in radio networks (assign frequencies to antennas with some slack, that is, an antenna can be assigned the same frequency with up to Δ* other antennas within its range without a signal conflict).

We will present some algorithmic and complexity results on this problem in classes of graphs where proper coloring is easy: on the one hand, we will consider subclasses of perfect graphs, namely cographs and chordal graphs; on the other hand we will talk about structural parameterizations, such as treewidth and feedback vertex set.

Joint work with Rémy Belmonte (University of Electro-Communications, Tokyo) and Michael Lampis (Lamsade, Université Paris Dauphine) that appeared in WG '17 and in STACS '18.

Séminaire des doctorants

mercredi 21 mars 2018, 11h00, Salle 3052

**Mengchuan Zou** (Theory and algorithmics of graphs team) *Generalization of binary search in trees and other structures*

The tree search problem is the following generalization of the binary search problem. A search strategy is required to locate an unknown target node t in a given tree T. Upon querying a node v of the tree, the strategy receives as a reply an indication of the connected component of T \ {v} containing the target t. The cost of querying each node is given by a known non-negative weight function, and the considered objective is to minimize the total query cost for a worst-case choice of the target.

We will also introduce some known facts on other structures and how tree search problem is related to other problems via equivalences.

Vérification

vendredi 23 mars 2018, 14h30, Salle 3052

**Javier Esparza** (Tecnhische Universität München) *One Theorem to Rule Them All: A Unified Translation of LTL into omega-Automata*

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into omega-automata by elementary means. In particular, the breakpoint, Safra, and ranking constructions used in other translations are not needed.

Joint work with Jan Kretinsky and Salomon Sickert.

Automates

vendredi 23 mars 2018, 14h30, Salle 3052

**Javier Esparza** (Technical University of Munich) *One Theorem to Rule Them All: A Unified Translation of LTL into omega-Automata*

We present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into omega-automata by elementary means. In particular, the breakpoint, Safra, and ranking constructions used in other translations are not needed.

Joint work with Jan Kretinsky and Salomon Sickert.