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

Lundi 29 mai 2017 · 14h00 · Salle 3052

Analyse et conception de systèmes · Silvia Crafa (Università di Padova) · Formal methods in action: typestate-oriented actor programming in Scala-Akka

Typestate-oriented programming is an extension of the OO paradigm in which objects are modelled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object’s internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. In this talk we examine a “full stack development”: we skip through a process calculus of actors equipped with a behavioural type system that allows to declare, to statically check and to infer state-based protocols, and we see it in action on Scala Akka programs, showing how far the standard Scala compiler supports protocol checking and discussing current work on compiler extension.

Mercredi 31 mai 2017 · 11h00 · Salle 3052

Séminaire des doctorants · Clément Jacq (PPS team) · TBA

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.