Gérald Point

Ingénieur de Recherches
CNRS
Département
M2F
Équipe
Modèles & Technologies pour la Vérification
Fonction administrative
Page personnelle
http://dept-info.labri.fr/~point
Adresse E-mail
gerald.point[at]labri.fr
Bureau
260
Tel
+33 (0)5 40 00 38 76

Recherche

Rattaché au thème Modélisation et Vérification de l'équipe MF mes activités portent actuellement sur deux axes de recherche: le projet AltaRica et la représentation symbolique de systèmes infinis.

<b>Le projet AltaRica</b>: Ce projet a pour objectif le développement d'outils d'analyse et de compilateurs pour le langage de modélisation AltaRica. Sur ce thème mon rôle est d'intégrer au logiciel ARC les techniques développées dans MV afin de proposer à nos partenaires industriels un outil stable. Principales caractéristiques de ARC:
. Langage AltaRica étendu aux propositions de l'ACI Persée
. mu-calcul modal pour la spécification des propriétés calculées
. Représentation exhautive ou symbolique des espaces d'états des modèles AltaRica
. Compilation vers d'autres langages (p.ex. Scade/Lustre dans le cadre du projet européen ISAAC).

<b>La logique de Presburger et les systèmes infinis:</b> La logique de Presburger permet de décrire facilement des systèmes comportant un nombre infini d'états. Les ensembles d'états décrits dans cette logique peuvent être représentés symboliquement par des automates reconnaissant des mots binaires. Nous développons une suite d'outils autour cette logique et de la manipulation des automates binaires:
. API générique pour la manipulation d'ensembles définissables en logique de Presburger
. Définition/compilation d'un langage de haut-niveau, Armoise, pour la description d'ensembles
. Implementation des Automates Partagés
Un résultat important sur ce thème est l'implémentation du résultat de J. Leroux sur la synthèse de formules de Presburger à partir d'un automate binaire.

Extrait de publications

Administration

Depuis 2016: Assistant de Prévention (AP)
2007 à 2010: Agent Chargé de la Mise en Oeuvre des règles d'hygiène et sécurtié (ACMO)