Institut de Recherche en Informatique Fondamentale

IRIF Université Paris 7 CNRS L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot, issue de la fusion des deux UMR LIAFA et PPS au 1er janvier 2016.

Ses objectifs scientifiques se déclinent selon trois grandes thématiques au cœur de l'informatique : les fondements mathématiques de l’informatique ; les modèles de calcul et de preuves ; la modélisation, les algorithmes et la conception de systèmes.

Prochains séminaires

Mercredi 07 décembre 2016 · 11h00 · Salle 1007

Combinatoire énumérative et analytique · Cedric Boutillier (UPMC) · ??

Vendredi 09 décembre 2016 · 14h30 · Salle 1006

Automates · Benjamin Hellouin (IRIF) · Computing the entropy of mixing tilings

The entropy of a language is a measure of its complexity and a well-studied dynamical invariant. I consider two related questions: for a given class of languages, can this parameter be computed, and what values can it take?

In 1D tilings (subshifts) of finite type, we have known how to compute the entropy for 30 years, and the method gives an algebraic characterisation of possible values. In higher dimension, a surprise came in 2007: not only is the entropy not computable in general, but any upper-semi-computable real number appears as entropy - a weak computational condition. Since then new works have shown that entropy becomes computable again with aditionnal mixing hypotheses. We do not know yet where the border between computable and uncomputable lies.

In this talk, I will explore the case of general subshifts (not of finite type) in any dimension, hoping to shed some light on the finite type case. I relate the computational difficulty of computing the entropy to the difficulty of deciding if a word belongs to the language. I exhibit a threshold in the mixing rate where the difficulty of the problem jumps suddenly, the very phenomenon that is expected in the finite type case.

This is a joint work with Silvère Gangloff and Cristobal Rojas.

Vendredi 09 décembre 2016 · 11h00 · Salle 3052

Vérification · Alastair Donaldson (Imperial College London) · Exposing Errors Related to Weak Memory in GPU Applications

In this presentation, I will describe a project led by my PhD student Tyler Sorensen, on the systematic design of a testing environment that uses stressing and fuzzing to reveal errors in GPU applications that arise due to weak memory effects. This approach is evaluated across several CUDA applications that use fine-grained concurrency, on seven GPUs spanning three Nvidia architectures. The results show that applications that rarely, or never, exhibit errors related to weak memory when executed natively can readily exhibit these errors when executed in the testing environment. The testing environment also provides a means to identify the root causes of erroneous weak effects, and automatically suggests how to insert fences that experimentally eliminate these errors. This empirical fence insertion method carries significantly lower overhead, in terms of execution time and energy consumption, than a more conservative, guaranteed-sound approach.

Lundi 12 décembre 2016 · 11h00 · Salle 2014

Combinatoire énumérative et analytique · Francois Nunzi (IRIF) · Soutenance de these: Autour de quelques chaines de Markov Combinatoires

Rapporteurs: M. Dukes et J.F. Marckert. Examinateurs: F. Bassino, J. Bouttier, P. Chassaing, S. Corteel, A. Sportiello, V. Ravelomanana

Lundi 12 décembre 2016 · 11h00 · Salle 1007

Vérification · Bin Fang (IRIF(Paris), ECNU (China)) · Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators (a logic-based approach)

We propose a hierarchical abstract domain for the analysis of free list memory allocators that tracks shape and numerical properties about both the heap and the free lists. Our domain is based on Separation Logic extended with predicates that capture the pointer arithmetics constraints for the heap list and the shape of the free list. These predicates are combined using a hierarchical composition operator to specify the overlapping of the heap list by the free list. In addition to expressiveness, this operator leads to a compositional and compact representation of abstract values and simplifies the implementation of the abstract domain. The shape constraints are combined with numerical constraints over integer arrays to track properties about the allocation policies (best-fit, first-fit, etc). Such properties are out of the scope of the existing analyzers. We implemented this domain and we show its effectiveness on several implementations of free list allocators.

Mardi 13 décembre 2016 · 11h00 · Salle 1007

Algorithmes et complexité · Amos Korman (CNRS, IRIF) · From Ants to Query Complexity

I will talk about my recent adventures with ants. Together with biologists we study P. longicornis ants as they collaboratively transport a large food item to their nest. This collective navigation process is guided by pheromones which are laid by individual ants. Using a new methodology to detect scent marks, we identify a new kind of ant trail characterized by very short and dynamic pheromone markings and highly stochastic navigation response to them. We argue that such a trail can be highly beneficial in conditions in which knowledge of individual ants regarding the underlying topological structure is unreliable. This gives rise to a new theoretical search model under unreliable guiding instructions, which is of independent computational interest. To illustrate the model, imagine driving a car in an unknown country that is in the aftermath of a major hurricane which has randomly flipped a certain small fraction of the road-signs. Under such conditions of unreliability, how can you still reach your destination fast? I will discuss the limits of unreliability that allow for efficient navigation. In trees, for example, there is a phase transition phenomenon that occurs roughly around 1/sqrt{D}. That is, if noise is above this threshold then any algorithm cannot avoid finding the target in exponential time (in the original distance), while below the threshold we identify an optimal, almost linear, walking algorithm. Finally, I will discuss algorithms that under such a noisy model aim to minimize the number of queries to find a target (rather than the number of moves).

This talk is based on joint works with biologists: Ofer Feinerman, Udi Fonio, Yael Heyman and Aviram Gelblum, and CS co-authors: Lucas Boczkowski, Adrian Kosowski and Yoav Rodeh.

Mardi 13 décembre 2016 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Hang Zhou (Max Planck Institute for Informatics) · Graph Reconstruction and Verification

How efficiently can we find an unknown graph using shortest path queries between its vertices? This is a natural theoretical question from the standpoint of recovery of hidden information. This question is related to discovering the topology of Internet networks, which is a crucial step for building accurate network models and designing efficient algorithms for Internet applications.

In this talk, I will introduce the problems of graph reconstruction and verification via oracles. I will investigate randomized algorithms based on a Voronoi cell decomposition. I will also analyze greedy algorithms, and prove that they are near-optimal.

The talk is based on joint work with Claire Mathieu and Sampath Kannan.