Gérald Point

Ingénieur de Recherches

CNRS

Department

M2F

Team

Modèles & Technologies pour la Vérification

Administrative function

Personal page

http://dept-info.labri.fr/~point

E-mail address

gerald.pointlabri.fr

Office

260

Tel

+33 (0)5 40 00 38 76

Research

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.

Excerpt from publications

• Fabien Kuntz, Stéphanie Gaudan, Christian Sannino, Éric Laurent, Alain Griffault, et al.. Model-based diagnosis for avionics systems using minimal cuts. DX 2011, Oct 2011, Murnau, Germany. pp.138-145.
• Alain Griffault, Gérald Point, Fabien Kuntz, Aymeric Vincent. Symbolic computation of minimal cuts for AltaRica models. 2011.
• Jérôme Leroux, Gérald Point. TaPAS : The Talence Presburger Arithmetic Suite. TACAS, 2009, York, United Kingdom. pp.182-185,
• Gérald Point, Alain Griffault. On the partial translation of Lustre programs into the AltaRica language and vice versa. 2006.
• Sébastien Bardin, Jérôme Leroux, Gérald Point. FAST Extended Release. Computer Aided Verification, CAV'06, Aug 2006, Seattle, WA, United States. pp.63-66.

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)