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.


Poste de maître de conférences


Un poste de maître de conférences est ouvert au concours 2017, affecté à l'IRIF, sur les thématiques de l'unité. Consulter la fiche de poste.


Prochains séminaires


Mercredi 31 mai 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Clément Jacq (PPS team) · A playful introduction to game semantics (category-light)

(English abstract below)

Une introduction ludique à la sémantique des jeux (allégée en catégories)

La sémantique des jeux est une branche de la théorie des modèles dont l'objectif est d'interpréter des formules de certaines logiques sous forme de jeux à deux joueurs. Son objectif initial était de lier les notions de vérité et de validité à des concepts de théorie des jeux tels que l'existence de stratégies gagnantes…

Après quelques exemples historiques, nous nous intéresserons dans cet exposé de manière informelle à un cas plus récent ou la sémantique des jeux modélise désormais des langages de programmation.

En guise de conclusion, nous évoquerons l'aspect formel avec la notion de structure catégorielle.


A playful introduction to game semantics (category-light)

Game semantics is a branch of model theory that aims at interpreting formulas of a given logic as two-player games. Initially, it was developed to link the notions of truth and validity to game-theoretic notions such as the existence of winning strategies.

After an historical example, we will look informally at a more recent case of game semantics where the games are used to model programming languages.

At the end, we'll mention the formal part with the notion of categorical model.


Jeudi 01 juin 2017 · 10h30 · Institut Henri Poincare

Combinatoire énumérative et analytique · Irène Marcovici, Elie De Panafieu, Jean-Christophe Aval (Universite de Lorraine, Nokia (Bell Labs), CNRS Labri) · Seminaire Flajolet


Jeudi 01 juin 2017 · 11h00 · Salle 3052

Vérification · Orna Grumberg (Technion, Israel) · Sound and Complete Mutation-Based Program Repair

This work presents a novel approach for automatically repairing an erroneous program with respect to a given set of assertions. Programs are repaired using a predefined set of mutations. We refer to a bounded notion of correctness, even though, for a large enough bound all returned programs are fully correct. To ensure no changes are made to the original program unless necessary, if a program can be repaired by applying a set of mutations $Mut$, then no superset of $Mut$ is later considered. Programs are checked in increasing number of mutations, and every minimal repaired program is returned as soon as found.

We impose no assumptions on the number of erroneous locations in the program, yet we are able to guarantee soundness and completeness. That is, we assure that a program is returned iff it is minimal and bounded correct.

Searching the space of mutated programs is reduced to searching unsatisfiable sets of constraints, which is performed efficiently using a sophisticated cooperation between SAT and SMT solvers. Similarities between mutated programs are exploited in a new way, by using both the SAT and the SMT solvers incrementally.

We implemented a prototype of our algorithm, compared it with a state-of-the-art repair tool and got very encouraging results. This is a joint work with Bat-Chen Rothenberg.


Vendredi 02 juin 2017 · 14h30 · Salle 1006

Automates · Michaël Cadilhac (U. Tübingen) · TBA


Vendredi 02 juin 2017 · 14h00 · Salle 1007

Catégories supérieures, polygraphes et homotopie · Léonard Guetta · Quelques remarques sur les modèles acycliques, d'après M.Barr


Mardi 06 juin 2017 · 11h00 · Salle 3052

Vérification · Sergio Rajsbaum (UNAM Mexico) · Tasks, objects, and the notion of a distributed problem

The universal computing model of Turing, which was central to the birth of modern computer science, identified also the essential notion of a problem, as an input output function to be computed by a Turing machine. In distributed computing, \emph{tasks} are the equivalent of a function: each process gets only part of the input, and computes part of the output after communicating with other processes.

In distributed computing tasks have been studied from early on, in parallel, but independently of \emph{sequential objects}. While tasks explicitly state what might happen when a set of processes run concurrently, sequential objects only specify what happens when processes run sequentially. Indeed, many distributed problems considered in the literature, seem to have no natural specification neither as tasks nor as sequential objects. I will concentrate on our recent work on interval-linearizability, a notion we introduced to specify objects more general than the usual sequential objects. I will describe the bridges we establish between these two classical paradigms, and our discussions about what is a distributed problem, and what it means to solve it.


Mardi 06 juin 2017 · 14h00 · Salle 3052

Sémantique · Jean-Bernard Stefani (INRIA) · Location graphs

This talk introduces location graphs, a new computational model for dynamic software architectures that supports sharing and encapsulation. The location graph framework draws on ideas developed in the last two decades around process calculi for distributed systems and dynamic services, as well as more informal ideas developed over the same period of time in software architecture and component-based software engineering. We present some results on location graph refinement and equivalence and discuss the relation of the location graph model with other formalisms.


Événements