IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université Paris-Diderot, also hosting two INRIA project-teams.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

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

(randomized-priority ranking)

IRIF Distinguished Talks

5.3.2019
The Collège de France and IRIF are delighted to host as part of our IRIF Distinguished Talks Series Robert Tarjan (Princeton) on March 18, 17:00 for a talk entitled “Concurrent Connected Components”

Uri Zwick

15.3.2019
From March 20th to May 22nd, Uri Zwick (Univ. of Tel Aviv) will give a series of 7 courses related to his FSMP Chaire of Excellence on the topic of Games on Graphs and Linear Programming Abstractions each Wednesday 2:15pm - 4:15pm at IRIF, room 3052.

14.3.2019
FSMP offers 21 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 2019. Applicants must be international students, but master students already in France for less than a year are eligible.

logo-cirm.jpg

5.11.2018
Amélie Gheerbrand and Cristina Sirangelo from IRIF co-organize with L. Libkin, L. Segoufin, and P. Senellart, the 2019 Spring School on Theoretical Computer Science (EPIT) on Databases, Logic and Automata, to happen the 7-12 April 2019 in Marseille. Preregistration before 13 January 2019.

Amaury Pouly

8.1.2019
IRIF has the great pleasure to welcome a new researcher (CNRS), Amaury Pouly, an expert in continuous models of computations, and the analysis and verification of continuous/hybrid dynamical systems.

Ile de France

17.3.2019
The Paris Region PhD2 program will grant 30 PhD projects on Digital Sciences and with an industrial partner. IRIF is an eligible hosting lab. Call for application is open until May, 15th 2019.

17.1.2019
Pierre Fraigniaud from IRIF organizes the Workshop Complexity and Algorithms (CoA), in the framework of GdR IM, Roscoff, France, April 1-5, 2019. The objective of this workshop is to gather the French community on design and analysis of algorithms, of all forms. Deadlines: submission by 01/02/2019, registration by 02/03/2019.

Uri Zwick

1.2.2019
IRIF has the great pleasure to welcome Uri Zwick, professor at the Blavantik School of Computer Sience (University of Tel-Aviv), who is visiting for four months. His stay is financed by an FSMP chair. Uri is an expert in algorithms, data structures and games. Meet him in office 4048.

IRIF seminar
Monday March 18, 2019, 5PM, Amphithéâtre Guillaume Budé - Marcelin Berthelot - Collège de France
Robert Tarjan (Princeton University and Intertrust Technologies) IRIF Distinguished Talks Series: Concurrent Connected Components

Finding the connected components of a graph is one of the most basic graph problems. Although it is easy to find components sequentially using graph search or a disjoint set union algorithm, some important applications require finding the components of huge graphs, making sequential algorithms too slow. We describe recent progress on concurrent algorithms for this problem. Some simple algorithms seem surprisingly hard to analyze, and claims made in the literature about some of them are false.

This talk is organized in collaboration with the Collège de France.

Verification
Monday March 18, 2019, 11AM, Salle 1007
Glen Mével (INRIA Paris) Time Credits and Time Receipts in Iris

I present a machine-checked extension of the program logic Iris with time credits and time receipts, two dual means of reasoning about time. Whereas time credits are used to establish an upper bound on a program’s execution time, time receipts can be used to establish a lower bound. More strikingly, time receipts can be used to prove that certain undesirable events—such as integer overflows—cannot occur until a very long time has elapsed. I will present a simple machine-checked application of time receipts, and sketch how we define our extension of Iris (and prove its soundness) in a modular way, as a layer above Iris.

Semantics
Monday March 18, 2019, 2PM, Salle 3052
Michel Schellekens (University College Cork) Expedient Algebra: Duality and Entropy Conservation

We introduce a new type of algebra, the Expedient Algebra EXP, for which computations satisfy tight distribution control. Algorithms satisfying such distribution control are guaranteed to support modular time analysis–drastically simplifying static timing. The property ensures that problematic algorithms, for which the exact time is too hard or impossible to analyze with current means can be distinguished at code level from algorithms supporting an elegant modular time analysis. Little is known about the intrinsic properties of algorithms exhibiting such distribution control.

We show that EXP-computations, made reversible through history-keeping, act as closed systems in which entropy is conserved. Thus modularity of timing is linked to entropy conservation of data flow, sharpening traditional entropy preservation guaranteed by the second law of thermodynamics for reversible systems. This type of conservation typically holds for the case of energy, but not for entropy. A salient point is that for algorithms satisfying distribution control, entropy is neither created nor destroyed, merely transferred from one form, i.e. quantitative entropy, to another, i.e. positional entropy.

We establish the Entropy Conservation Laws ECL-1 and ECL-2. ECL-1 expresses the inverse proportionality of positional and quantitative entropy for distributions over series-parallel orders and their duals. ECL-2, a computational version of entropy conservation, expresses that order established by the expedient product (with history) on labels is proportionally destroyed on indices by a shadow transformation in the dual space. The laws shed new light on the properties of algorithms for which distribution control, and hence modular timing, is guaranteed.

Logic, automata, algebra and games
Wednesday March 20, 2019, 2:15PM, 3052
Uri Zwick (Blavatnik School of Computer Science) Games on Graphs and Linear Programming Abstractions, Part 1/7: Two-player Turn-based Stochastic Games

In the first lecture we define the two-player Turn-Based Stochastic Games (TBSGs), the most general games considered in this lecture series. We define the objectives of the two players, the strategies that they can use, and define the values of the games. We then consider algorithms for finding the values and optimal strategies, first in one-player games and then in two-player games. While for one-player games polynomial time algorithms are known, for most two-player games no polynomial time algorithms are currently known.

https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf

Special talks
Wednesday March 20, 2019, 1PM, Salle 3052
Lin Chen (LRI) Algorithm Design and Analysis in Wireless Networks

Algorithms are one of the most fundamental elements in computer science. Networks and networked systems are no exception. In this talk, I will present our recent research on some algorithmic problems of both fundamental and practical importance in modern networks and networked systems, more specifically, wireless networks. Methodologically, most of our analysis is systematically articulated as follows: (1) Establishment of theoretical performance bound, (2) Optimum or approximation algorithm design, (3) Further extension and generalization. Our objective is to make a tiny while systematic step forwards in the design and analysis of algorithms that can scale elegantly, act efficiently in terms of computation and communication, while keeping operations as local and distributed as possible.

Proofs, programs and systems
Thursday March 21, 2019, 10:30AM, Salle 3052
Paolo Pistone (Univ. Tubingen) Quelques résultats sur l'équivalence des preuves dans la logique linéaire du second ordre

Les réseaux de preuves donnent une représentation canonique des démonstrations dans la logique linéaire multiplicative : l'équivalence dénotationnelle des preuves coïncide avec l'équivalence des réseaux. Par contre, la canonicité des réseaux ne s'étend pas au second ordre. Ce problème est du à la présence des témoins des règles existentielles. En fait, dans plusieurs sémantiques dénotationnelles l'information portée par les preuves est compressée, et notamment les témoins existentiels sont effacés.

Font partie de ces sémantiques “effaçantes” les sémantiques cohérente et rélationnelle, ainsi que la sémantique dinaturelle et la sémantique observationnelle. On présente des résultats sur l'équivalence des preuves dans ces sémantiques et on discute des applications en complexité dues à la possibilité de compresser les preuves. Une partie de ces travaux est issue d'une collaboration avec L. Tortora de Falco, T. Seiller et L.T.D. Nguyễn.

Special talks
Thursday March 21, 2019, 1PM, Salle 3052
Reem Yassawi (Université de Lyon) Les automates cellulaires et dynamique symbolique

Les automates cellulaires sont des objets qui peuvent être interprétés, d’un point de vue informatique, comme modèles de calculs parallèles, ou d’un point de vue mathématique, comme systèmes dynamiques. Ils forment donc un pont entre deux domaines de science apparement éloignés. Je donne un bref survol de la théorie des automates cellulaires en dynamique symbolique. Ensuite j’expose deux problèmes différents autour des automates cellulaires auxquels je me suis intéressée.

Le premier problème concerne les propriétés de randomisation de certains automates cellulaires. La randomisation asymptotique est le processus par lequel un état initial de basse entropie est asymptotiquement transformée en un état d'entropie maximale, par l’action itérée de l’automate cellulaire. Je discute des conditions nécessaires et suffisantes pour qu’une telle randomisation survienne, et aussi d'un travail récent avec Eric Rowland.

La deuxième problématique est de caractériser les automates cellulaires qui préservent un langage donné. Je résume un travail récent avec Clemens Muellner, où nous obtenons un théorème de structure pour les automates cellulaires qui préservent certains langages HD0L.

IRIF Cake
Thursday March 21, 2019, 5:30PM, in front of room 3052
Simon Maurras (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Automata
Friday March 22, 2019, 2:30PM, Salle 3052
Reem Yassavi (CNRS, Institut Camille Jordan - Université Lyon 1 - Claude Bernard) Versions quantitatives du théorème de Christol

Pour une suite a = (a_n)_{n≥0} à valeurs dans un corps fini F_q, le théorème de Christol établit une équivalence entre q-automaticité de a (a calculable par un automate) et l’algebricité de la série formelle f(x) = \sum a_n x^n. Dans ce travail nous étudierons le nombre d’états de l’automate en fonction des paramètres du polynôme annulateur minimal de f(x).

Andrew Bridy a récemment donne une démonstration du théorème de Christol en utilisant des outils qui proviennent de la géométrie algébrique. Avec cette démonstration il majore le nombre d’états par une borne qui est optimale. Nous obtenons des bornes presque semblables par une démonstration élémentaire, et nous traçons les liens entre notre démonstration et celle de Bridy. Ceci est un travail en commun avec Boris Adamczewski.

Verification
Friday March 22, 2019, 11AM, 3052
Matteo Maffei (TU Wien) Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts

The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics.

This talk will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust, a framework for the static analysis of Ethereum smart contracts that we recently designed, which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first steps towards a static analysis for EVM bytecode, based on Horn clause resolution, that comes with a proof of soundness.

Graphs
Friday March 22, 2019, 2PM, Salle 1007
Julien Baste (Universität Ulm, Ulm, Germany) Hitting minors on bounded treewidth graphs

For a fixed collection of graphs F, the F-DELETION problem consists in, given a graph G and an integer k, decide whether there exists S, subset of V(G), with |S| ⇐ k such that G-S does not contain any of the graphs in F as a minor. This NP-hard problem is a generalization of some well known graph problems as VERTEX COVER (F={K_2}), FEEDBACK VERTEX SET (F={K_3}), or VERTEX PLANARIZATION (F={K_5,K_{3,3}}). We are interested in its parameterized complexity when the parameter is the treewidth of G, denoted by tw. Namely, the objective is to determine, for a fixed F, the (asymptotically) smallest function f_F: N → N such that F-DELETION can be solved in time f_F(tw)*n^{O(1)} on n-vertex graphs. In this talk we will provide the basic definitions of parameterized complexity, motivate the problem, and then, review some of the lower and upper bounds on the function f_F for several instantiations of F.

The presented results are joint work with Ignasi Sau and Dimitrios Thilikos and can be found in <https://arxiv.org/abs/1704.07284>.

Verification
Monday March 25, 2019, 11AM, Salle 1007
Cristoph Kirsch (Universität Salzburg) On the Self in Selfie

Selfie is a self-contained 64-bit, 10-KLOC implementation of (1) a self-compiling compiler written in a tiny subset of C called C* targeting a tiny subset of 64-bit RISC-V called RISC-U, (2) a self-executing RISC-U emulator, (3) a self-hosting hypervisor that virtualizes the emulated RISC-U machine, and (4) a prototypical symbolic execution engine that executes RISC-U symbolically. Selfie can compile, execute, and virtualize itself any number of times in a single invocation of the system given adequate resources. There is also a simple linker, disassembler, debugger, and profiler. C* supports only two data types, uint64_t and uint64_t*, and RISC-U features just 14 instructions, in particular for unsigned arithmetic only, which significantly simplifies reasoning about correctness. Selfie has originally been developed just for educational purposes but has by now become a research platform as well. We discuss how selfie leverages the synergy of integrating compiler, target machine, and hypervisor in one self-referential package while orthogonalizing bootstrapping, virtual and heap memory management, emulated and virtualized concurrency, and even replay debugging and symbolic execution.

This is joint work with Alireza S. Abyaneh, Simon Bauer, Philipp Mayer, Christian Mösl, Clément Poncelet, Sara Seidl, Ana Sokolova, and Manuel Widmoser, University of Salzburg, Austria.

Web: http://selfie.cs.uni-salzburg.at