Projets

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.

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.

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.

Il s’agit de : - concevoir la syntaxe pour la hiérarchie et les liens père-fils, avec une attention particulière sur les variables et horloges globales/locales - interfacer dans CosyVerif avec cette structure hiérarchique (à plusieurs niveaux) - traduire en réseau d’automates

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.

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.

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é.

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.