Laboratoire Méthodes Formelles

Quantum computing can be thought of in multiple ways. Among those ways, it can be seen as a computational model of quantum mechanics. Studying this model may have implications for our understanding of physics. It can also be seen as a new computational paradigm, with implications for computation, algorithms, and logic. Additionally, it can be viewed as a computational device that requires programming. Therefore, it is necessary to design and study programming languages for this purpose. The study of the foundations of quantum programming languages, type theory, and logic through the Curry-Howard correspondence may shed light on our understanding of quantum mechanics. Furthermore, it may lead to the development of new logics or the understanding of new structures in classical logic. Lastly, implementing these languages will enhance the way we program the new computers when they become widely used. In this project, we propose to study these various aspects of quantum computing, specifically focusing on the foundations of programming languages.

Les bases de données relationnelles font face à la complexité des données interconnectées et hétérogènes. Ainsi, les bases de données graphes ont gagné en popularité dans l'industrie et l'académie. Par exemple, certaines avec des données multiomiques ont été collaborativement conçues pendant la pandémie pour des analyses génomiques et le traçage de contacts (EU Datathon, CovidGraph, Covid-19 Knowledge Graph). Finance, télécommunications, journalisme et transports intelligents sont d'autres utilisations critiques sociétales. Cependant, le traitement à grande échelle de graphes géo-distribués nécessite des modèles qui posent encore des défis : la réplication, pour gérer des réseaux lents et peu fiables, le partitionnement, pour répartir de grands graphes, et la réplication partielle à proximité des clients, pour la localité. Aussi, les modèles local-first offrent une haute disponibilité, combinant partitionnement et réplication, pour accéder à une partie pertinente de données en cas de déconnexion. Si les mécanismes de distribution, tels que les types de données répliqués (RDT), sont utilisés par des bases clés-valeurs local-first, pour les bases de données graphes leur usage est largement inexploré. Cela est plus difficile, car il nécessite la maintenance des invariants de connectivité complexes compositionnels. VERDI propose une méthodologie interdisciplinaire pour concevoir des RDT graphes (GRDT) fiables, recoupant les domaines des bases de données, des systèmes distribués, des méthodes formelles et des langages de programmation. Il comprend quatre packages de travail (WP). WP1 fournira un fondement formel unifié pour le prototypage et l'extraction des GRDT corrects par construction. WP2 les adaptera pour assurer la préservation des invariants complexes dans des modèles à faible cohérence. WP3 étendra les GRDT avec la paramétricité et les transactions, et WP4 évaluera leurs performances sur le cas industriel d’un registre décentralisé basé sur des graphes.

La conception et vérification formelles de systèmes critiques exigent de considérer avec la même importance, dès le début, les exigences fonctionnelles et temporelles. Néanmoins, intégrer le temps sous toutes ses formes dans les assistants de preuves reste un défi majeur car le temps est souvent intégré tard, après plusieurs niveaux de raffinement et de manière manuelle et ad-hoc. D'un autre côté, il y a de nombreux modèles de temps riches et variés qui ont chacun leur expressivité et leurs limites mais qui intègrent peu ou pas les exigences fonctionnelles. Nous distinguons le temps des autres propriétés non-fonctionnelles car beaucoup d'autres propriétés sont interdépendantes du temps (énergie, chaleur, sécurité) et le temps prend une importance particulière dans les systèmes hybrides ou systèmes cyber-physiques dont certaines parties dont décrites par des équations différentielles. Ce projet propose des outils et une méthodologie pour combiner Event-B à des outils de vérification automatique de propriétés temporelles et promeut le temps comme un citoyen de premier niveau. D'un côté, cela augmente l'efficacité des assistants de preuve sur les propriétés temporelles qui peuvent être établies efficacement par des model-checkers. D'un autre, cela repousse les limites des outils de vérification automatique par l'utilisation de preuves sur des modèles paramétriques, lorsque la preuve généralise sur un domaine un résultat sans nécessiter l'exploration exhaustive (explicite ou symbolique) du domaine. Ceci constitue une innovation majeure pur la vérification des systèmes critiques en combinant les avantages des deux communautés qui à ce jour, progressent essentiellement séparément.

En situations critiques, les opérateurs doivent poser des diagnostics provisoires sur la base d'informations partielles et incertaines pour prendre des décisions. Ce contexte est propice aux « erreurs de fixation », c’est-à-dire le fait de ne pas mettre à jour l'évaluation d'une situation ou de persister dans un plan d'action qui n'est plus approprié. Ces erreurs sont une cause majeure d'événements indésirables et d'accidents dans les domaines de la santé et de l'aviation commerciale. Le projet IDEFIX a pour objectif d'étudier l'apport de l'Intelligence Artificielle et de la Réalité Virtuelle & Augmentée pour aider les opérateurs en situation critique, comme des pilotes d'avion ou des professionnels de santé, à détecter ces erreurs de fixation et à développer des stratégies pour les prévenir et minimiser leur impact. Pour ce faire, nous allons étudier le comportement de pilotes et de soignants dans des environnements simulés, construire une représentation en logique formelle de la situation, développer un assistant informatique capable de d’identifier de possibles erreurs de fixation et mesurer l’impact de l’utilisation de ce dispositif sur la performance des opérateurs. Nous utilisons donc une approche pluridisciplinaire qui combine des recherches en sciences humaines (facteurs humains et psychologie cognitive) et en informatique (intelligence artificielle, interaction humain-machine, réalité virtuelle pour la formation). Nos contributions en SHS portent sur la compréhension des mécanismes d'apparition des erreurs de fixation, à partir d'études terrain. Nos contributions en informatique portent sur la conception d'un modèle formel de diagnostic de l'erreur humaine et son utilisation dans un contexte de formation en réalité virtuelle et augmentée. Ce projet a pour objectif de contribuer à augmenter la sécurité dans les domaines de l’aviation et de la santé.

À mesure que la taille et la complexité des circuits génétiques synthétiques augmentent, ils deviennent progressivement trop lourds pour une seule cellule. Par conséquent, de nombreux circuits génétiques de démonstration sont facilement perdus par sélection négative lorsque les organismes modifiés sont exposés à des environnements moins contrôlés. En revanche, les systèmes naturels sont capables de porter des programmes génétiques beaucoup plus importants en utilisant des mécanismes de régulation complexes pour contrôler les coûts d'expression. Ils y parviennent par une combinaison de contrôle temporel sur l'expression des gènes et, en outre, par la distribution spatiale des fonctions dans les systèmes multicellulaires. Dans ce projet, nous prévoyons de développer des méthodes expérimentales et théoriques pour mesurer le coût du maintien et de l'exécution des circuits génétiques synthétiques à l'intérieur des cellules. Des modèles quantitatifs seront construits pour calculer le coût d'expression, et l'effet sur la croissance, de protéines uniques et de circuits multiprotéiques au fil du temps. Les modèles seront étudiés dans différentes conditions de croissance et de stress afin d'évaluer la relation entre les coûts calculés et la stabilité évolutive à long terme des circuits. Les analyses permettront de faire des choix de conception pertinents pour construire les circuits unicellulaires les plus rentables, et de déterminer la limite supérieure de taille à laquelle il serait plus efficace de les répartir sur plusieurs cellules dans un consortium. Nous nous attendons à ce que les résultats de ce travail aient des implications clés non seulement pour la mise à l'échelle des circuits génétiques synthétiques, mais aussi pour la compréhension des fonctions de l'écosystème dans les communautés microbiennes et la division du travail dans les organismes multicellulaires.

Les technologies quantiques utilisent des ressources non-classiques comme la superposition et l’intrication pour obtenir un avantage quantique. On a compris récemment qu’il est également possible de tirer un avantage computationnel de structures causales fondamentalement quantiques. Cette "indétermination causale" s'avère être une nouvelle ressource, ouvrant une perspective inédite en information quantique. Toutefois, malgré certains progrès théoriques et expérimentaux, les implications concrètes de ces recherches pour le calcul quantique ne sont pas encore suffisamment bien comprises. Dans ce projet, nous développerons la compréhension de l’indétermination causale afin de l’établir fermement en tant que nouvelle ressource non-classique, au même titre que la superposition et l’intrication. Pour cela, nous suivrons trois voies. 1) Nous travaillerons sur les théories probabilistes généralisées, afin de mieux comprendre l’indétermination causale en la plaçant dans une classe plus large de modèles. Cette analyse clarifiera le caractère physique des processus causalement indéterminés, ainsi que le rôle précis des ressources non-classiques. 2) Au-delà du cadre désormais standard du "quantum switch", nous étudierons des modèles plus concrets du calcul causalement indéterminé. Cela nous permettra d’explorer de manière systématique les applications de l’indétermination causale et de mieux saisir son potentiel. 3) Nous utiliserons enfin le "calcul ZX" pour tirer profit du caractère non-classique de l’indétermination causale au niveau de la compilation. Ici, le langage ZX permettra d’aller plus vite vers la programmation des calculs causalement indéfinis, permettant d’optimiser l’utilisation de cette nouvelle ressource. Ces trois volets œuvrent pour un même objectif ultime, qui consiste à formuler les bons arguments dans le bon langage afin de donner à l’indétermination causale toute sa place parmi les principaux paradigmes conceptuels et empiriques de l’information quantique.

Les systèmes informatisés sont omniprésents et l'identification de leurs défauts est cruciale dès les premières phases de développement, quand de nombreux aspects, comme les environnements d'exécution, n'ont pas encore été fixés. La vérification doit alors se faire sur des systèmes sous-spécifiés et, de façon contradictoire, apporter des réponses aussi informatives que possible. Dans ce projet, nous développons des techniques de vérification pour ces systèmes, en prenant en compte ce besoin d'explicabilité, par l'optimisation de ressources telles que l'énergie ou la mémoire, et la synthèse de contraintes sur les aspects sous-spécifiés, garantissant le bon fonctionnement du système. Au delà des formalismes classiques, nous considérons leurs extensions simultanées dans trois directions: des coûts pour les ressources, des paramètres pour les caractéristiques inconnues, et des jeux pour représenter tous les comportements du systèmes sous-spécifié. Le problème principal des formalismes très expressifs que nous voulons étudier et promouvoir, est que les problèmes de vérification et de synthèse associés sont très complexes, au sens algorithmique du terme, ce qui se traduit par une utilisation du processeur et de la mémoire rédhibitoires en pratique. Les problèmes de décision liés sont aussi le plus souvent indécidables. Pour attaquer ce problème, nous suivons deux approches complémentaires. D'une part, et c'est la voie la plus souvent explorée pour ce type de situations, nous identifions deux sous-classes du formalisme général qui modélisent bien certaines applications ciblées et pour lesquelles nous pensons pouvoir obtenir de meilleurs résultats théoriques et pratiques D'autre part, nous proposons le développement d'algorithmes spécifiques fonctionnant sur le formalisme général mais aux résultats fournissant des résultats approchés accompagnés de garanties formelles sur l'approximation réalisée.

Le projet GOSPEL vise à enrichir la définition de Gospel, un langage de spécification pour OCaml; à développer un écosystème d'outils basés sur Gospel; et à effectuer un certain nombre d'études de cas permettant d'éprouver expérimentalement l'utilisabilité de Gospel. Gospel permet d'annoter du code OCaml avec une spécification qui décrit comment ce code est utilisé et quel service il rend. Cette spécification est ensuite utilisée par divers outils pour engendrer de la documentation, effectuer des tests automatisés, et vérifier la correction fonctionnelle de ce code. Gospel vise à devenir un standard de fait, que les programmeurs peuvent apprendre aisément, et que les outils peuvent adopter comme base commune. Nous choisissons OCaml parce qu'il offre une combinaison unique de simplicité, de pouvoir expressif, d'efficacité, et de stabilité à long terme, et parce qu'il est utilisé dans le monde universitaire et dans l'industrie pour développer des logiciels complexes et critiques. Comparé à des langages de plus bas niveau, OCaml supprime plusieurs sources potentielles de comportement aberrant, ce qui facilite la vérification de programmes, mais propose également des moyens puissants pour assembler un programme à partir de composants élémentaires, ce qui rend la spécification plus difficile. Nous souhaitons démontrer que Gospel permet de détecter des erreurs auxquelles le système de types d'OCaml est insensible, d'où une sûreté accrue pour un surcoût limité. Nos principaux objectifs sont de: 1. Développer le langage Gospel, de façon à accroître son pouvoir expressif, tout en préservant sa simplicité. 2. Développer l'écosystème des outils fondés sur Gospel, dont le typeur de Gospel, l'IDE Merlin, et des outils de documentation, de test, et de vérification. 3. Éprouver Gospel et en démontrer l'intérêt via des études de cas, allant de bibliothèques simples jusqu'à des composants logiciels complexes tirés d'applications industrielles critiques.

Les progrès récents dans la conception de bactéries synthétiques génétiquement modifiées ont un impact potentiel élevé sur les nouvelles solutions de calcul biologique par les bactéries, telles que les applications de biodétection, la bioproduction et les médicaments intelligents. Ce projet de recherche propose des solutions innovantes au problème de la construction de circuits distribués dans les bactéries d'un point de vue algorithmique et théorique qui contribue à des solutions réalisables dans le monde réel. Nous envisageons les résultats attendus suivants : De nouveaux algorithmes robustes et une meilleure compréhension des décisions de conception : L'analyse mathématique des algorithmes distribués a deux objectifs principaux : elle établit des limites de correction et de performance et permet d'évaluer systématiquement les décisions de conception algorithmique. Les implémentations biologiques et leur environnement étant intrinsèquement sujets au bruit et aux erreurs, la robustesse à ces effets est essentielle pour les algorithmes distribués. Les exigences concrètes sont la robustesse aux variations des paramètres du modèle (par exemple, en raison de la variabilité entre les cellules bactériennes) et à une fraction des bactéries qui ne suivent pas l'algorithme (par exemple, en raison de mutations de perte de fonction). Nouveaux blocs de construction : Tout algorithme repose essentiellement sur les primitives/blocs de construction disponibles. Pour les algorithmes distribués, les primitives de communication sont centrales. Nous allons concevoir, mettre en œuvre et vérifier expérimentalement un nouveau système basé sur les phages pour transférer l'ADN d'une bactérie à une autre.

La conception d'un système informatique complexe peut être gérée par un haut degré de modularité, qui joue un rôle déterminant dans la maintenance d'un système tout au long de sa vie (mises à jour et reconfigurations). Ces systèmes contrôlent des aspects importants de notre vie, d'où l'importance d'assurer leur bon comportement en utilisant des modèles formels et des techniques de vérification. Ce projet fournit une base pour la conception et la vérification de systèmes complexes, basés sur les notions de ressource et de composition. Par ressource, nous entendons tout composant (physique ou logique) d'un système et par composition toute modalité d'interaction entre composants. Les opérateurs de composition doivent donc être plus généraux que de simples compositions agrégatives (unions disjointes). Nous allons concevoir des logiques englobant ces notions générales de compositions non agrégatives et définir de modèles pour la conception et la vérification.