2017 | PeRSPECTiVE

Axe :Scilex
Coordinateurs : Évelyne Contejean et Stéphane Demri
Objectif : Le rapprochement du LSV avec VALS, permettra de constituer une masse critique d’environ 50 permanents et être l’amorce d’un pôle de recherche de visibilité internationale dans le domaine de l’informatique fondamentale et particulièrement celui de la spécification, de la démonstration, du test formel et de la vérification.
Financement Labex : 2017
Documents


Présentation :
La source de ce GT prend son origine avec le GT Sasefor qui relevait du champ général des méthodes formelles et couvrait un périmètre bien plus large.

L’arrivée imminente (2018-2019) de l’École Normale Supérieure de Cachan et de son laboratoire d’informatique, le LSV, à quelques mètres du LRI, commande d’approfondir des échanges déjà nourris.

Il s’agit de réfléchir sur un projet scientifique coordonné entre le LSV, l’équipe VALS du LRI et l’équipe Toccata de l’INRIA, en explorant leurs proximités et complémentarités scientifiques, en nouant des collaborations, qui auront vocation à se concrétiser par des publications, des projets communs, des co-encadrements de stage ou de thèse.

Depuis octobre 2016, un séminaire commun a lieu, une fois tous les deux mois, en alternance entre Cachan (le mardi matin) et Orsay (le vendredi matin), avec deux exposés par séance, l’un donné par un membre du LSV, l’autre par un membre de VALS. L’ensemble des thématiques VALS/LSV seront invitées.


Séminaires

  • 28 octobre 2016 – Amphi du bâtiment 660 – LRI:
    • Chantal Keller (LRI) : Interoperability between proof systems: the triumvirate of automation, expressivity, and safety
    • Gilles Dowek (LSV) : Dedukti : de la revérification à la réingénierie des preuves
  • 31 janvier 2017 – Amphi Chemla, Institut d’Alembert, ENS Cachan:
    • David Baelde (LSV) – XPath with data : a uniform and effective approach through proof theory
    • Kim Nguyễn (LRI) – A principled approach to language-integrated queries (Quelques lambdas dans un monde de brutes)
  • 31 mars 2017 – LRI – grand amphi du PUIO bat 640:
  • 23 mai 2017 – LSV – amphi Chemla, Institut d’Alembert:
    • Laurent Fribourg (LSV) – Synthèse de contrôle pour des systèmes gouvernés par des équations différentielles en utilisant la méthode d’Euler
    • Sylvie Boldo (LRI) – Arithmétique flottante et résolution d’équations différentielles

Équipes concernées

  • CNRS & ENS Paris-Saclay
    • DEDUCTEAM,
    • INFINI,
    • MEXICO,
    • SECSI et VASCO du LSV
  • CNRS & Université Paris-Sud
    • VALS du LRI
    • TOCCATA, INRIA Saclay Île-de-France

Post-Docs Adossés

FAC – Full Abstraction for Languages with Demonic and Probabilistic Choice 

Axe & tâche scientifique DigiCosme : SciLex
Coordinateurs :Jean-Goubault Larrecq, LSVEvelyne Contejean, LRI
Nom & Prénom du Candidat : Zhenchao LIU
Adresse mail :
Laboratoire gestionnaire: LSV
Page web


ATOM – Attack Tolerance using Machine learning and Big Data 

Axe & tâche scientifique DigiCosme : SciLex
Coordinateurs :Fatiha Zaïdi, LRIAna Rosa Cavalli, SAMOVAR
Nom & Prénom du Candidat :
Adresse mail :
Laboratoire gestionnaire: LRI
Page web