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.4.2020
The first virtual workshop co-organized by a member of IRIF, Valérie Berthé, took place March 23-27 on Multidimensional Continued Fractions and Euclidean Dynamics. All talks have been recorded and are publicly accessible.

7.4.2020
All seminars of IRIF are now active again through BigBlueButton, an open source solution installed on our local servers thanks to our amazing staff support. Check out our page about seminars for more information.

7.4.2020
The OCaml MOOC developed by Ralf Treinen, Roberto Di Cosmo and Yann Régis-Gianas from IRIF is reopened during COVID19 sheltering. Use this time at home to learn functional programming!

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

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.

(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).

Automates
Vendredi 10 avril 2020, 14 heures 30, Online
Javier Esparza An Efficient Normalisation Procedure for Linear Temporal Logic

Joint work with Salomon Sickert

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of LTL with past operators is equivalent to a formula of the form $\bigwedge_{i=1}^n \G\F \varphi_i \vee \F\G \psi_i$, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for the future fragment of LTL. Both normalisation procedures had a non-elementary worst-case blow-up, and followed an involved path from LTL formulas to counter-free automata to star-free regular expressions and back to LTL. We improve on both points. We present a purely syntactic normalisation procedure from LTL to LTL, with single exponential blow-up, that can be implemented in a few dozen lines of Standard ML code. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

Online seminar on BigBlueButton

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.

Graphes
Mardi 14 avril 2020, 15 heures 30, Online
Pierluigi Crescenzi (IRIF) Temporal Closeness in Temporal Networks

The closeness centrality measure associates to each node of a graph its average distance from all the other nodes. In this talk, we will consider a temporal version of this measure, which have been recently introduced and analysed in the case of temporal graphs (that is, graphs in which edges can appear and disappear during time). In particular, we will show how this measure can be efficiently approximated by using a “backward” temporal breadth-first search algorithm and a classical sampling technique. We will then introduce a “temporally global” closeness centrality measure of a node in a temporal graph, which is quite similar to the notion of AUC (Area Under Curve), and we will show how this global measure can also be efficiently approximated. We conclude by presenting several experimental results in the case of medium/large real-world temporal networks. This is a joint work with Clémence Magnien and Andrea Marino.

Vérification
Mercredi 15 avril 2020, 15 heures, (online, using BigBlueButton)
Akos Hajdu (Budapest University of Technology and Economics) SMT-Friendly Formalization of the Solidity Memory Model

Solidity is the dominant programming language for smart contracts on the Ethereum blockchain. This talk presents a high-level formalization of the Solidity language with a focus on the memory model. The memory model of Solidity has various unusual and non-trivial behaviors, providing a fertile ground for potential bugs. Smart contracts have access to two classes of data storage: a permanent storage that is a part of the global blockchain state, and a transient local memory used when executing transactions. While the local memory uses a standard heap of entities with references, the permanent storage has pure value semantics (although pointers to storage can be declared locally). This memory model that combines both value and reference semantics - with all interactions between the two - poses some interesting challenges but also offers great opportunities for automation. The presented formalization covers all features of the language related to managing state and memory in an effective way: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the solc-verify tool and we provide an evaluation on an extensive test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.

Combinatoire énumérative et analytique
Jeudi 16 avril 2020, 14 heures, Online
Viviane Pons (Université Paris-sud) Involution “Montée - Contacts” sur les intervalles de Tamari

Nous présentons une involution sur les intervalles de Tamari qui échange deux séries de statistiques : les “montées” et les “contacts”. Cette involution fait intervenir de nombreux objets combinatoires : chemins de Dyck, arbres, intervalles-posets.