L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris-Diderot, qui héberge deux équipes-projets INRIA.

Les objectifs scientifiques de l'IRIF se situent au cœur de l'informatique, et plus particulièrement sur la conception, l'analyse, la preuve et la vérification d'algorithmes, de programmes et de langages de programmation. Ils s'appuient sur des recherches fondamentales développées à l'IRIF en combinatoire, graphes, logique, automates, types, sémantique et algèbre.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), et deux sont membres de l'Institut Universitaire de France (IUF).

21.03.2018
The next meeting of the ANR project DESCARTES, aiming at defining a modular approach for distributed computing, will take place at IRIF on March 28, 2018. Scientific talks are public.

20.03.2018
The next meeting of the ANR project DELTA, conducting research about the new challenges in Logic, Automata and Transducers, will take place at University Paris Diderot from 2018/03/26 to 2018/03/28. Scientific talks are public.

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.​

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.

Vérification
lundi 26 mars 2018, 11h00, Salle 1007
Ivan Gazeau (LORIA & INRIA Nancy - Grand Est) Automated Verification of Privacy-type Properties for Security Protocols

The applied pi-calculus is a powerful framework to model protocols and to define security properties. In this symbolic model, it is possible to verify automatically complex security properties such as strong secrecy, anonymity and unlinkability properties which are based on equivalence of processes. In this talk, we will see an overview of a verification method used by a tool, Akiss. The tool is able to handle

- a wide range of cryptographic primitives (in particular AKISS is the only tool able to verify equivalence properties for protocols that use xor);

- protocols with else branches (the treatment of disequalities is often complicated).

We will also provide some insights on how interleaving due to concurrency can be effectively handled.

Graphes
mardi 27 mars 2018, 14h00, Salle 1007
Matej Stehlik (Université Grenoble Alpes - GSCOP) Nombre chromatique et la méthode topologique

La méthode topologique est la seule méthode connue pour déterminer le nombre chromatique de certaines classes de graphes, et un problème classique est d’obtenir des preuves alternatives plus élémentaires. Après une brève introduction à la méthode topologique, je présenterai certains de mes travaux qui y sont liés et j’expliquerai pourquoi le recours à la topologie est parfois difficilement évitable.

Algorithmes et complexité
mardi 27 mars 2018, 11h00, Salle 1007
Kamil Khadiev (University of Latvia) Quantum online algorithms with restricted memory

An online algorithm is a well-known computational model for solving optimization problems. The defining property of this model is following. An algorithm reads an input piece by piece and should return output variables after some of the input variables immediately, even if the answer depends on the whole input. An online algorithm should return output for minimizing an objective function.

We consider streaming algorithms and two-way automata as models for online algorithms. We compare quantum and classical models in case of logarithmic memory and sublogarithmic memory.

We get the following results for online streaming algorithms: - a quantum online streaming algorithm with 1 qubit of memory and 1 advice bit can be better than a classical online streaming algorithm with $o(\log n)$ bits of memory and $o(\log n)$ advice bits. - Quantum online streaming algorithm with a constant size of memory and $t$ advice bits can be better than deterministic online streaming algorithms with $t$ advice bits and unlimited computational power. - In a case of a polylogarithmic size of memory, quantum online streaming algorithms can be better than classical ones even if they have advice bits.

We get the following results for two way automata as an online algorithm for solving online minimization problems: - a two way automata with quantum and classical states for online minimization problems with a constant size of memory can be better than classical ones even if they have advice bits.

Séminaire des doctorants
mercredi 28 mars 2018, 11h00, Salle 3052
Yann Hamdaoui (Proofs and Programs and Conception and Analysis of Systems teams) TBA

Combinatoire énumérative et analytique
jeudi 29 mars 2018, 11h45, Salle 1007
Melissa Sherman-Bennett (Berkeley) Combinatorics of X-variables in finite type cluster algebras

Cluster algebras were introduced by Fomin and Zelevinsky in the early 2000s, with the intent of establishing a general algebraic structure for studying dual canonical bases of semisimple groups and total positivity. A cluster algebra is a commutative ring determined by an initial “seed,” which consists of A-variables, X-variables, and some additional data. One then applies a combinatorial process called mutation to this seed to obtain another seed. The cluster algebra is generated by the variables obtained from all possible sequences of mutations. In this talk, we will focus on cluster algebras of finite type, which are those with finitely many A- and X-variables. There is a complete classification of finite type cluster algebras due to Fomin and Zelevinsky, which coincides with the classification of reduced crystallographic root systems. For classical types, the combinatorics of the A-variables and their mutations are encoded by triangulations of marked surfaces associated to each type. In particular, seeds are in bijection with triangulations, and A-variables are in bijection with the arcs of the triangulations. In this talk, we will discuss new results on the combinatorics of the X-variables in finite type cluster algebras. We will show that in classical types, the X-variables are in bijection with the quadrilaterals (with a choice of diagonal) appearing in triangulations of the surface of the appropriate type. Using this bijection, we can then count the number of X-variables in each type, as well as obtain some corollaries regarding the structure of finite type cluster algebras.

Preuves, programmes et systèmes
jeudi 29 mars 2018, 10h30, Salle 3052
Guilhem Jaber (LIP) TBA