Projets

Ajouter

#	Titre	Résumé	Type	Frequence	Durée	Laboratoire
2	La réduction basée sur l'ordre partiel pour le PMC-SOG	Le PMC-SOG est un model-checker parallèle basé sur le graphe d'observation symbolique (SOG). Il reçoit en entrée un graphe de l'espace d'état d'un système et une propriété LTL et vérifie à la volée de manière parallèle et/ou distribuée si le système satisfait la propriété. Le PMC-SOG est implémenté en C++ et utilise la bibliothèque des threads de C++ et MPI.	prototype	2 jours/semaine	6 mois	LIPN
3	Folding for rewriting modulo SMT	We have recently shown how rewriting-modulo-SMT can be an appropriate semantic framework for the specification and verification of real-time systems. Applications include the definition of interpreters for Parametric Timed Automata and Parametric Time Petri Nets. The results are promising and the implementation of the rewrite theories in Maude show that our methods can be used in practice, outperforming in some cases state-of-the-art tools in the field. The analysis of real-time system in Maude requires the definition of a folding procedure for guaranteeing termination when the parametric zone graph is finite. Such a procedure checks when two symbolic states, possibly syntactical different, define the same set of concrete states. This project aims at improving the efficiency of our rewrite tools by implementing, at the C++ level of Maude, a general folding procedure to guarantee termination. Currently, this procedure is implemented at the meta-level of Maude.	prototype	2 jours/semaine	3 mois	LIPN
4	Structures de données modulaires dans IMITATOR	IMITATOR est un outil de model-checking temporisé paramétré, permettant de synthétiser des valeurs de paramètres temporels pour lesquels une propriété est vérifiée. IMITATOR repose sur une bibliothèque de polyèdres, une structure de données très appropriée pour les modèles paramétrés. En revanche, pour les modèles non paramétrés (automates temporisés classiques, sans paramètres ni stopwatches), les polyèdres sont trop coûteux, et de simples DBMs (difference bound matrices) suffiraient amplement.	prototype	2 jours/semaine	6 mois	LIPN
8	Automation for Coq in SMTCoq	SMTCoq, and its extension Sniper <https://smtcoq.github.io/sniper>, is a long term project to automatically call automatic solvers from the Coq proof assistant. Tomaz will start with basic software engineering tasks to get familiar with the architecture of the project, in particular porting to the last version of Coq. Then the main objective of the project is to validate the new goal encoder of Sniper by implementing new transformations, such as the encoding of refinement types, and defunctionalization, time permitting.	maintenance/évolution logiciel existant	2 jours/semaine	6 mois	LMF
9	LLMTypeInfer	The reconstruction of set-theoretic types for dynamic languages can be prohibitively time-consuming. Our current prototype, [CDuce DynLang](https://www.cduce.org/dynlang/), takes an untyped program written in an "idealized" dynamic language, reconstructs an annotation tree for the program, and checks its typing. Although checking whether an annotation tree makes a program well-typed is extremely fast, the reconstruction of the annotation tree can be very slow. The goal of this project is to optimize the type inference process by fine-tuning a Large Language Model (LLM) to produce a (possibly partial) annotation tree for a program. The type-checker will subsequently verify the annotation tree, resorting to the slower reconstruction only if the check fails. By integrating the fine-tuned LLM into the type inference process, we aim to significantly reduce the time required for reconstructing set-theoretic types in dynamic languages while maintaining a high level of accuracy.	proof-of-concept	2 jours/semaine	4 mois	IRIF
10	Autosubst2	Autosubst2 est un plugin Coq/Rocq qui sert à aider les formalisations de langages avec des variables liées, en générant des lemmes "boilerplate" pour la représentation des variables en indices de De Bruijn. (Page web : https://www.ps.uni-saarland.de/extras/autosubst2/ ) Je propose de compléter l'implémentation de Autosubst2 pour faciliter les formalisation Rocq de langages de programmation.	proof-of-concept	2 jours/semaine	2 mois	IRIF

Terminés

#	Titre	Résumé	Type	Frequence	Durée	Laboratoire
1	Modèles templates/paramétrés dans IMITATOR	IMITATOR est un outil de model checking temporisé paramétré, permettant de synthétiser des valeurs de paramètres temporels pour lesquels une propriété est vérifiée. Parmi les manquements actuels, l'outil ne peut pas instancier des templates (ou modèles paramétrés), par exemple, afin de construire un système à partir de n instances d'un modèles (1 serveur et 10 clients, par exemple). Le projet permettra d'ajouter cette fonctionnalité à l'outil.	prototype	2 jours/semaine	6 mois	LIPN
5	Set-theoretic types with CDuce	Le projet CDuce consiste en un compilateur pour un langage statiquement typé, fonctionnel, basé sur le sous-typage sémantique. Cette discipline de typage sophistiquée offre une grande souplesse au programmeur qui peut par exemple tester dynamiquement le type des valeurs manipulées. En termes simples, ils permet d’alier la souplesse des langages dynamiques tels que Python ou Javascript à la sûreté du typage offerte par des langages comme OCaml.	maintenance/évolution logiciel existant	2 jours/semaine	3 mois	LMF
6	Jeux de tests pour babeld	Il existe plusieurs implémentations du protocole Babel, dont deux sont utilisées en production : babeld, implémenté à l'IRIF, et BIRD. Babeld est un logiciel stable, mais il n'inclut pas de jeux de tests, ce qui fait que chaque changement au code doit être soigneusement vérifé.	maintenance/évolution logiciel existant	2 jours/semaine	3 mois	IRIF
7	Usuba	Usuba is a high-level domain-specific programming language to write high-throughput and constant-time cryptographic primitives, generating low-level C (+ SIMD intrinsics) code, and based on a generalization of bitslicing that we call m-slicing.	prototype	2 jours/semaine	2 mois	IRIF