Contact : Dominique Barth, David, UVSQ, Benedikt Bollig, LSV, ENS Paris Saclay
Les programmes sont très utiles et facilitent grandement notre vie. Malheureusement, ils ne sont pas entièrement fiables. Ils ont souvent des “bugs”. Le développement et l’utilisation des logiciels ont considérablement évolué ces dernières années. L’évolution principale vient de l’explosion des communications. C’est à la fois une opportunité et une menace. L’axe SciLex du Labex DigiCosme est d’appréhender la fiabilité et la sécurité des systèmes d’information et de communication de demain. Ce travail de recherche s’articule autour de 3 grands thèmes :
- 1 – Utilisation et sureté des programmes distribués.
- 2 – Systèmes continus et discrets : modèles et vérification
- 3 – Certification
Tous ces thèmes se retrouvent dans les différents projets financés par le Labex DigiCosme.
1 – Projets Emergence
- CODECSYS – 2016
- Coordination : Antoine Girard – CentraleSupelec, L2S
- Thème : Contract Based Design of Cyber-Physical Systems
- VERICONISS – 2014
- Coordination : Stefan Göller – ENS ParisSaclay, LSV
- Thème : Verification of Concurrent Infinite State Systems
2 – Groupes de Travail
- GT UPScaLe – 2017 – 2019
- Contact :Chantal Keller, LRI , Frédéric Blanqui, Inria
- Thème : Utiliser les preuves comme protocoles de communication entre systèmes de preuves
- GT HicDiesMeus – 2017 – 2019
- Contacts :Thomas Nowak, LRI, Matthias Függer, LSV
- Thème : Étudier des problèmes d’ordre physique, biologique ou sociologique dans un contexte d’informatique distribuée
- GT TheoBioR – 2016 – 2019
- Contacts : Loïc Paulevé, LRI, Stefan Haar, LSV
- Thème : Méthodes informatiques pour la modélisation et l’analyse des réseaux biologiques
- GT PeRSPECTiVE – 2017 – 2018
- Contacts : Evelyne Contejean, LRI, Stéphane Demri, LSV
- Thème : Recherche fondamentale sur : spécification, démonstration, du test formel et de la vérification
- GT SDT – 2016 – 2017
- Contacts : Cyril Grouin, LIMSI, Catuscia Palamidessi, LIX, Olivier Ferret, CEA list
- Thème : Sécurité des Données Textuelles
- GT OVSTR – 2015 – 2017
- Contacts : Mathieu Jan, CEA list, Florian Brandner, LTCI, Laurent Pautet, LTCI
- Thème : Optimisation des Systèmes Temps Réel.
- GT Combinatoire – 2015 – 2017
- Contacts : Vincent Pillaud, Marie Albenque, LIX, Florent Hivert, LRI
- Thème : Combinatoire énumérative, géométrique et algébrique.
- GT ELFIC – 2014 – 2016
- Contacts : Sylvie Boldo, LRI, Eric Goubault, LIX
- Thème : Preuve de correction de la bibliothèque FELiScE implantant la méthode des éléments finis pour la résolution numérique d’équations aux dérivées partielles
- GT SHy – 2013 – 2015
- Contacts : Alexandre Chapoutot, Ensta PrisTech, Catherine Bonnet, L2S, Paolo Masson, L2S
- Thème : Les diverses approches des systèmes dynamiques et hybrides
3 – Thèses
- Discobole – Distributed computation for blockchain with long term security – 2019
- Directeur de thèse : Matthieu Rambaud, LTCI
- Doctorant : Angelo Saadeh
- Institution : Telecom Paris
- ROTOR – Algorithmic properties of rotor walks in graphs, and related decision models – 2019
- Directeur de thèse : Pierre Coucheney, DAVID
- Doctorant : Loric Duhaze
- Institution : UVSQ
- EPITA – External Provers In Proof Assistants – 2017
- Directeur de thèse : Frédéric Blanqui
- Doctorant : Mohamed Yacine El Haddad
- Institution : Inria
- Xeres – Information Exposure by Error Signalling – 2017
- Directeur de thèse : Dietmar Berwanger
- Doctorant : Mengqi Xie
- Institution : ENS PARIS-SACLAY
- Compositional controller synthesis for hybrid systems – 2016
- Directeur de thèse : Antoine Girard
- Doctorant : Adnane SAOUD
- Institution : CentraleSupelec
- AlgoReCell – 2016
- Directeur de thèse : Stefan Haar
- Doctorant : Hugues Mandon
- Institution : ENS PARIS-SACLAY
- ELEFFAN project – 2016
- Directeur de thèse : Sylvie Boldo
- Doctorant : Florian Faissole
- Institution : LRI
- Ergo Fast – 2015
- Directeur de thèse : Sylvain Cochon
- Doctorant : Albin Coquereau
- Institution : Université Paris Sud
- DisMonTest – 2015
- Directeur de thèse : Stéphane Maag
- Doctorant : Jose Alfredo Alvarez-Aldana
- Institution : Telecom SudParis
4 – Post-Doc – Ingénieurs
- LFAT – Linking Focusing and Automated Theorem Proving – 2019-2020
- Chercheur postdoctoral : Matteo Acclavio
- Institution : Telecom SudParis
- PREGARI – Commande PREdictive Garantie Robuste aux Incertitudes – 2019-2020
- Chercheur postdoctoral :
- Institution : ENS PARIS-SACLAY
- TacticTHo – Tactiques de preuve pour formaliser des modèles de la théorie des types homotopiques en déduction modulo réécriture – 2019-2020
- Chercheur postdoctoral : Rehan Malak
- Institution : ENS Paris-Saclay
- ATOM – Attack Tolerance using Machine learning and Big Data – 2019-2020
- Chercheur postdoctoral :
- Institution : Université Paris Sud
- DynaRNA – Dynamics of RNA – 2018-2019
- Chercheur postdoctoral : Christelle Rovetta
- Institution : Université Paris Sud
- FAC – Full Abstraction for Languages with Demonic and Probabilistic Choice
- Chercheur postdoctoral : Zhenchao LIU
- Institution : ENS PARIS-SACLAY
- DafPUP – Domain Approximations for Programs with Uncertain Probabilities – 2018-2019
- Chercheur postdoctoral : Jia, Xiaodong
- Institution : ENS PARIS-SACLAY
- DIGIT – Distributed Pulse Generation in Bacterial Colonies – 2018-2019
- Chercheur postdoctoral : Da-Jung Cho
- Institution : ENS PARIS-SACLAY
- CODECSYS – Contract Based Design of Cyber-Physical Systems – 2017-2019
- Chercheurs postdoctoraux : Lucien Etienne, Alina Eqtami
- Institution : CentraleSupelec
- SaSeFor – Méthodes Formelles – 2017-2018
- Chercheurs postdoctoraux : Valentin Blot, Maha Naceur
- Institution : ENS PARIS-SACLAY
- TheoBioR – Méthodes informatiques pour la modélisation et l’analyse des réseaux biologiques – 2017-2018
- Chercheur postdoctoral : Eva Dechaux
- Institution : Université Paris Sud
- VERICONISS – Verification of Concurrent Infinite State Systems – 2014-2016
- Chercheurs postdoctoraux : Christoph Haase, Piotr Hofman
- Institution : ENS PARIS-SACLAY