Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet 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. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois 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.

Suivez nous sur Mastodon, Twitter/X et LinkedIn :

LinkedIn Twitter/X Mastodon

dts_omer_reingold.jpg

10.4.2024
L'IRIF a le plaisir d'annoncer son deuxième Distinguished Talk de l'année ! Notre conférencier invité est Omer Reingold, professeur d'informatique à l'université de Stanford et directeur de la Simons Collaboration sur la théorie de l'Équité algorithmique (Simons Foundation). Il parlera de l'équité algorithmique. Toute personne intéressée est invitée à se joindre à nous pour cette conférence !

12.4.2024
La rediffusion de la conférence (en anglais) de Véronique Cortier, qui s'est tenue en février, est désormais disponible sur la chaîne YouTube de l'IRIF. Son sujet était : “Le vote électronique : conception et vérification formelle”.

logopintofscience2024.jpg

10.4.2024
Trois projets de médiation scientifique de chercheurs à l'IRIF ont été sélectionnés pour l'édition 2024 de Pint of Science France-Paris. Le principe : découvrir une thématique ou un sujet scientifique, dans un bar. Nos chercheurs parleront protection des données, graphes et informatique quantique.

mirna-dzamonja.jpeg

28.3.2024
La Société mathématique de Belgique (SMB) a décerné à Mirna Džamonja (CNRS, IRIF, Université de Paris) le “Prix Godeaux” de la SMB. “Ce prix est décerné chaque année, sur proposition d'un membre du conseil d'administration de la BMS, à un-e mathématicien-ne belge ou international-e de renom qui est invité-e à donner une conférence en Belgique”. Toutes nos félicitations !

tayssir_touili.jpg

27.3.2024
Nous accueillons une nouvelle directrice de recherche à l'IRIF, Tayssir Touili. Ses domaines d'intérêt sont la détection de logiciels malveillants, la vérification de logiciels et les méthodes formelles. Vous pouvez la rencontrer dans le bureau 4028A.

quentin_aristote.jpg

29.3.2024
Bravo à Quentin Aristote, doctorant, qui a reçu le prix Helena Rasiowa pour le meilleur papier étudiant, lors de la 32ème conférence EACSL : Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids.

marie-jose_iarifina.jpg

27.3.2024
Marie-Josée Iarifina a rejoint l'IRIF pour remplacer Natalia Hacquart en tant que gestionnaire financière et comptable. Venez la rencontrer et lui souhaiter la bienvenue dans le bureau 4002.

12.3.2024
Hugo Herbelin, directeur de recherche Inria à l'IRIF, organise la prochaine journée Horizon Maths sur le sujet : Preuve mathématique et sûreté logicielle. Elle aura lieu le mercredi 27 mars 2024 de 9h à 18h à l'institut Henri Poincaré (5 rue Pierre et Marie Curie, Paris 5e), amphithéâtre Hermite. Inscription gratuite mais obligatoire :


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

Catégories supérieures, polygraphes et homotopie
Vendredi 19 avril 2024, 14 heures, Salle 3058
Jovana Obradovic A Calculus for S^3-diagrams of Manifolds with Boundary

n this talk, we shall introduce a calculus for a presentation of compact, orientable, connected 3-manifolds with boundary in terms of diagrams embedded in S^3 in a form akin to the standard surgery presentation of closed, orientable, connected 3-manifolds. The motivation to introduce such a presentation of manifolds is to give a completely combinatorial description of the category 3Cob, whose arrows are 3-dimensional cobordisms, which is an ongoing project. We hope this could support further investigations of faithfulness of 3-dimensional Topological Quantum Field Theories.

This is a joint work with Bojana Femić, Vladimir Grujić and Zoran Petrić.

Automates
Vendredi 19 avril 2024, 14 heures, Salle 3052
Florent Capelli Direct Access For Conjunctive Queries with Negation

Direct Access is the operation of returning, given an index j, the j-th answer of a conjunctive query Q on a given database for some given order on the answers set of Q. While this problem is #P-hard in general (wrt combined complexity), many conjunctive queries are structured enough so that for some lexicographical ordering of their answers, one can have a direct access to the answer of Q that takes polylogarithmic time in the size of the database after polynomial time precomputation. Previous work have precisely characterized the tractable classes and given fine grained lower bounds on the time needed for precomputation depending on the structure of the query. We give a generalization of these tractability results to the case of signed conjunctive queries, that is, conjunctive queries that may contain negative atoms. Our technique is based on solving the ranked access for a class of circuits that can represent relational data. Our result then follows from the fact that the tractable (signed) conjunctive queries can be transformed into polynomial size circuit. We recover the known tractable classes from the literature in the case of positive conjunctive queries using this technique and also discover new island of tractability for signed conjunctive queries. In particular, our result generalizes to the Ranked Access Problem the known tractabilities of counting the number of answers to beta-acyclic negative queries and of deciding whether a negative query with bounded nested-width has an answer. This is join work with Oliver Irwin and appeared at ICDT 2024:

- ArXiv version: https://arxiv.org/abs/2310.15800 - Published version: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2024.13

Vérification
Lundi 22 avril 2024, 11 heures, 3052 (streamed) and Zoom link
Sidi Mohamed Beillahi (University of Toronto) Securing Smart Contracts Through Program Synthesis

In decentralized finance (DeFi), malicious adversaries were able to steal over 2 billions dollars in crypto assets over the past two years. One very common strategy malicious adversaries use is to borrow large assets through flash loans to launch their exploits against vulnerable DeFi smart contracts deployed on the Blockchain. Flash loans are loans that are only valid within a blockchain transaction and must be repaid with fees by the end of that transaction. Unlike normal loans, flash loans allow borrowers to borrow large assets without upfront collateral deposits.

In this talk, I will first present a work on automated synthesis of adversarial transactions that exploit DeFi smart contracts using flash loans. To bypass the complexity of a DeFi protocol and needs for source code analysis, we propose a new technique to approximate the DeFi protocol functional behaviors using numerical methods (polynomial linear regression and nearest-neighbor interpolation). We then construct an optimization query using the approximated functions of the DeFi protocol to find an adversarial attack that is constituted of a sequence of functions invocations with optimal parameters that provides the maximum profit. To improve the accuracy of the approximation, we propose a novel counterexample driven approximation refinement technique.

I will then present a followup work studying a category of DeFi attacks known as oracle manipulation attacks and the effectiveness of the current mechanisms used to protect against those attacks. I will show that those mechanisms are inadequate to ensure DeFi smart contracts safety when confronted with significant oracle deviations. I will then present a new framework to identify parameters that allow to secure DeFi smart contracts against oracle manipulation attacks. In the framework, we first perform symbolic analysis on the given contract and construct a summary model of constraints. We then leverage an SMT solver to identify parameters values that allow to secure smart contracts against oracle deviations.

The talk is based on two ICSE 2024 papers that are joint works with Zhiyang Chen, Xun Deng, Andreas Veneris, and Fan Long (University of Toronto) and Cyrus Minwalla and Han Du (Bank of Canada).

Algorithmes et complexité
Mardi 23 avril 2024, 11 heures, Salle 3052
Team Event AlgoComp lightning talks ⚡️

Algorithmique distribuée et graphes
Mardi 23 avril 2024, 14 heures, 3052 Sophie Germain
Cléophée Robin (G-Scop) Non encore annoncé.

One world numeration seminar
Mardi 23 avril 2024, 14 heures, Online
Shunsuke Usuki (Kyoto University) On a lower bound of the number of integers in Littlewood's conjecture

Littlewood's conjecture is a famous and long-standing open problem which states that, for every $(\alpha,\beta) \in \mathbb{R}^2$, $n\|n\alpha\|\|n\beta\|$ can be arbitrarily small for some integer $n$. This problem is closely related to the action of diagonal matrices on $\mathrm{SL}(3,\mathbb{R})/\mathrm{SL}(3,\mathbb{Z})$, and a groundbreaking result was shown by Einsiedler, Katok and Lindenstrauss from the measure rigidity for this action, saying that Littlewood's conjecture is true except on a set of Hausdorff dimension zero. In this talk, I will explain about a new quantitative result on Littlewood's conjecture which gives, for every $(\alpha,\beta) \in \mathbb{R}^2$ except on sets of small Hausdorff dimension, an estimate of the number of integers $n$ which make $n\|n\alpha\|\|n\beta\|$ small. The keys for the proof are the measure rigidity and further studies on behavior of empirical measures for the diagonal action.

Séminaire des membres non-permanents
Jeudi 25 avril 2024, 16 heures, Salle 3052
Etienne Objois A width-independent algorithm for approximating the $\ell_p$ norm of a nonnegative matrix and its applications.

Given a matrix $A$ with $m$ rows and $n$ columns, we want to approximate the maximum value of $||A x||_p$ when $||x||_q <= 1$. For general matrices, a $(1-\epsilon)$ approximation of the problem is hard, but for nonnegative matrices, when $q >= p >= 1$, the problem can be transformed into a concave maximization problem. In this talk, we will present a width-independent (i.e., the running time dependence on $n m$ is at most poly-logarithmic) algorithm to find $(1-\epsilon$) approximations in time nearly $O(nnz/\epsilon)$.

In the second part of the talk, we will see how such an algorithm can be used to compute competitive oblivious linear routings.

Algorithmique distribuée et graphes
Vendredi 26 avril 2024, 14 heures, 1020
Dimitri Watel (ENSIIE) Edit distance to a linegraph, application to network reconstruction

We consider the context of a network modeled by an undirected graph where the edges are known, but not the connections between these edges. This can happen in old buildings where, for example, an electrical, gas or water network has not been documented and where the network is not easily accessible. We may have access to some cables or pipes of the network either because they are visible or because it is possible to probe the building to find them. From the edges of the graph, we obtain measures of the probability that two edges are incident, in other words measures of the linegraph of the network, with possibly errors in the measurements. We aim to correct the errors by finding the linegraph closest to the measurement graph. This problem is modeled as an edit distance problem in terms of deleting and adding edges in a graph to retrieve a linegraph. We pose the question, firstly, of studying the complexity of correcting these errors and its parameterized complexity with respect to the number of possible errors and the treewidth of the graph, secondly, the relevance of such correction in relation to the desired graph based on the number of measurement errors, and thirdly, what other information could be added to the graph to aid in reconstruction as the number of measurement errors increases.

Vérification
Lundi 29 avril 2024, 11 heures, 3052 and Zoom link
Niklas Kochdumper (IRIF) Neural Network Verification using Polynomial Zonotopes

Since artificial intelligence is nowadays also increasingly applied in safety-critical applications such as autonomous driving and human robot collaboration, there is an urgent need for approaches that can efficiently verify that the corresponding neural networks are safe. In general, verification tasks involving neural networks can be classified into the two groups open-loop verification and closed-loop verification. For open-loop verification one aims to prove certain properties of a standalone neural network, while for closed-loop verification the neural network acts as a controller for a dynamic system. This presentation demonstrates a novel verification technique that is based on a polynomial abstraction of the input-output-relation of the single neurons, which proves to be beneficial for both open- as well as closed-loop neural network verification.

Combinatoire énumérative et analytique
Mardi 30 avril 2024, 11 heures, Salle 3058
Séminaire Reporté Pas de séance