Les membres de l'IRIF et les visiteurs sont priés de se conformer aux directives COVID-19 du CNRS et de l'Université de Paris.

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

Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), cinq sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences.

7.2.2020
IRIF will finance one or two additional Master scholarships in Foundations of Computer Science within the PGSM program of FSMP for female students who have completed a bachelor’s degree or the first year masters in one of the universities of the FSMP network. Apply by May 8th.

10.1.2020
Université de Paris has opened one permanent associate professor position in Computer Science. Recruited researcher will join IRIF. Apply by April 9th, 4pm (Paris time).

6.2.2020
Sylvain Périfel from IRIF, together with Damiano Mazza and Thomas Seiller, organize the Caleidoscope Research School in Computational Complexity, to be held in Paris (postponed to 2021).

(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Tous les évènements sont actuellement organisés à distance (ou suspendus).

Vérification
Lundi 6 avril 2020, 11 heures, (online, using BigBlueButton)
Amaury Pouly (CNRS & IRIF) Polynomial Invariants for Affine Programs and Introduction to Algebraic Geometry (for computer scientists)

In this talk I will present some results we obtained in LICS 2018 where we exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose assignments are given by affine expressions). Our main tool is an algebraic result of inde- pendent interest: given a finite set of rational square matrices of the same dimension, we show how to compute the Zariski closure of the semigroup that they generate.

I will then give a small introduction to algebraic geometry for computer scientisits. The goal it to give the background necessary to understand how the proof works: we will talk about algebraic sets/varieties and constructible/definable sets.

In a second talk on April 20th, I will give use the material introduced in this talk to explain the algorithm for computing the Zariski closure of a group and semigroup of matrices.

Graphes
Mardi 7 avril 2020, 15 heures 30, Online
Pierre Berge Fixed-parameter algorithms for finding small separators in graphs

In this talk, I introduce some results obtained during my Ph.D. All of them deal with cut and connectivity problems in graphs. I present the parameterized complexity of the Partial One-Target Cut (POTC) problem, where the objective is to identify the smallest edge cutset separating a certain proportion r of sources into an input set S={s_1,…,s_k} with a single target t. I provide the proof that POTC is fixed-parameter tractable (FPT) parameterized by the cutset size p. This means that an algorithm finds an exact solution in time f(p)P(n), where f is an arbitrary function, P a polynomial function, and n the instance size. The algorithm is based on the random sampling of important separators. This result highlights a surprising complexity gap between the edge and the vertex versions of the problem. Indeed, when the cutset is made up of vertices, POTC is unlikely to be FPT.

Séminaire des doctorants
Mercredi 8 avril 2020, 11 heures, Online
Nicolas Jeannerod (IRIF) Analysing installation scenarios of Debian packages

Debian GNU/Linux is a Linux distribution composed of free and open-source software. It is heavily used all over the world as an operating system for personal computers and servers, and is the basis for many other distributions.

Deban currently includes more than 28 thousand maintainer scripts, almost all of them written in POSIX shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. While Debian policy provides guidance for package maintainers producing the scripts, few tools exist to check the compliance of a script to it.

This presentation reports on the application of a formal verification approach based on symbolic execution to find violations of some non-trivial properties required by Debian policy in maintainer scripts. We present our methodology and give an overview of the toolchain. We focus in particular on the tree logics used to represent symbolically a file system transformation, and the use of such a logic in the symbolic engine.

Combinatoire énumérative et analytique
Jeudi 9 avril 2020, 14 heures, Online
Camille Combe (IRMA) To be announced

Preuves, programmes et systèmes
Jeudi 9 avril 2020, 14 heures, Online
Charles Grellois (Université d'Aix-Marseille) Non encore annoncé.

Algorithmes et complexité
Vendredi 10 avril 2020, 15 heures, Online
André Schrottenloher, Yixin Shen (INRIA, IRIF) Improved Classical and Quantum Algorithms for Subset-Sum

We present new classical and quantum algorithms for solving random hard instances of the subset-sum problem, in which we are given n integers on n bits and try to find a subset of them that sums to a given target. This classical NP-complete problem has several applications in cryptography and underlies the security of some proposed post-quantum cryptosystems. At EUROCRYPT 2010, Howgrave-Graham and Joux (HGJ) introduced the representation technique and presented an algorithm running in time $\tilde{O}(2^{0.337 n})$. This asymptotic time was improved by Becker, Coron, Joux (BCJ) at EUROCRYPT 2011. We show how to improve this further. We then move to the context of quantum algorithms. The two previous quantum speedups in the literature are given by Bernstein, Jeffery, Lange and Meurer (PQCRYPTO 2013) and Helm and May (TQC 2018), which are respectively quantum versions of HGJ and BCJ. They both rely on the framework of quantum walks, use exponential quantum memory with quantum random-access and require an unproven conjecture on quantum walk updates. We devise a new algorithm, using quantum search only, that achieves the first quantum speedup in the model of classical memory with quantum random access. Next, we study improvements for the quantum walks. We show how to avoid the quantum walk conjecture and give a better quantum walk time complexity for subset-sum.

Joint work with Xavier Bonnetain and Rémi Bricout.