Curriculum Vitæ

[nom]

A.T.E.R. à temps partiel de l’université de Nice – Sophia Antipolis, École Supérieur en Sciences Informatiques (ESSI)

Membre du projet COPRIN / CNRS (I3S)-INRIA-CERMICS

[date de naissance]

[information personnelle], nationalité française

[adresse]

Tél : [téléphone]

Mél : [e-mail]

Coordonnées professionnelles

École Supérieur en Sciences Informatiques

930, Route des Colles

[adresse] Antipolis, France

Tél : [téléphone]

Fax : [téléphone]

Mél : [e-mail]

Web : [lien]

Table des matières

Formation et parcours professionnel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

Activités pédagogiques . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

Activités de recherches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

Logiciels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

Recommandation professionnelles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

Formation et parcours professionnel

• 2002 : Thèse de doctorat de l’Université de Nice – Sophia Antipolis, « Généralisations et méthodes correctes pour l’induction mathématique » spécialité informatique, mention très honorable, soutenue le 29 mars 2002 à l’ESSI devant le jury composé de :
• Alain C OLMERAUER , Professeur Université de la Méditerranée, Président,
• Emmanuel K OUNALIS , Professeur UNSA, Directeur de recherche,
• Jürgen G IESL , Professeur RTWH Aachen, Rapporteur,
• Michaël R USINOWITCH , D.R. INRIA, Rapporteur,
• Zohar M ANNA , Professeur Stanford University,
• Michel R UEHER , Professeur UNSA,
• Robert DE S IMONE , D.R. INRIA.
• 1998 : DEA informatique, mention très bien, ESSI Mémoire : Preuves par Induction dans le Calcul de Situation
• 1997 : Maîtrise informatique, mention bien, Nice
• 1996 : Licence informatique, mention très bien, Nice

Postes universitaires

• 2002-2003 : A.T.E.R. à mi-temps

UNSA, École Supérieur en Sciences Informatiques.

• 2001-2002 : A.T.E.R. à mi-temps

UNSA, UFR Sciences, département informatique.

• 1998-2001 : Allocation de recherche (MESR) couplée à un monitorat UNSA, UFR Sciences, département informatique.

Centre d’Initiation à l’Enseignement Supérieur de Provence.

Tuteur pédagogique : Michel Rueher.

• 1996-1997 : Tutorat UNSA, DEUG MIAS.

Autres expériences professionnelles

• Août – Septembre 1995 : Réalisation d’un logiciel de gestion de stock.

France Télécom (Agence Magnan), Nice

• Juillet – Août 1994 : Stage dans l’équipe de support informatique.

Crédit Lyonnais Capital Market, London.

2

Activités pédagogiques

Dans le cadre de mon monitorat puis de mon poste d’ATER au département infor-matique de l’UNSA, j’ai effectué essentiellement des travaux pratiques et des travaux dirigés en premier cycle. J’ai aussi pu présenter un cours dans mon domaine de re-cherche en maîtrise d’informatique et plusieurs travaux dirigés en deuxième cycle.

Mon deuxième contrat d’ATER s’est déroulé à l’École Supérieur en Sciences In-formatiques (ESSI). L’ESSI est une école d’ingénieur dépendant de l’UNSA et com-mençant à BAC+3 assurant aussi des formations de 3ème cycle (DESS et DEA). Ayant une formation et un thème de recherche principal assez théorique, j’ai profité des op-portunités offertes par ce poste pour enseigner des technologies innovantes (JSP, EJB, XML, JDO, XSL, . . . ). J’ai pu appréhender rapidement ces technologies basées sur Java grâce à mes connaissance en langage objet acquises lors de ma formation et lors du développement des logiciels NICE et VOTE.

Détails UFR Sciences – premier cycle 1

Algorithmique

DEUG MI2 · T.P. · (13h)

Responsable : E. Kounalis ([e-mail])

Informatique et programmation (en java)

DEUG MIAS tronc commun · T.P. · (60h)

Responsable : J. Durand-Lose ([e-mail])

Outils formels pour l’informatique

DEUG MP1 · T.D. · (20h)

Responsable : B. Beauquier ([e-mail])

DEUG MI2 · T.D. · (24h)

Responsable : J-M. Fedou ([e-mail])

Programmation fonctionnelle (Scheme)

DEUG MI2 · T.D.M. (24h)

DEUG MP2 · T.D.M. (13h)

Responsable : J-P. Roy ([e-mail])

Programmation système et langage AWK

DEUG MASS2 · T.D.M. (26h)

Responsable : R. Rousseau ([e-mail])

Systèmes informatiques et réseaux

DEUG MP2 · T.P. · (12h)

Responsable : V. Granet ([e-mail])

Systèmes informatiques

DEUG MI2 · T.P. · (52h)

Responsable : O. Lecarme ([e-mail])

1

• MP : Mathématiques et Physique ; MI : Mathématiques et Informatique ; MASS : Mathématiques Ap- pliquées aux Sciences Sociales.
• T.P. : Travaux Pratiques ; T.D. : Travaux Dirigées ; T.D.M. : Travaux Dirigées sur Machine.

3

Détails UFR Sciences – deuxième cycle

Théorie et modèles, Logique

Licence informatique · T.D. · (12h)

Responsable : E. Kounalis ([e-mail])

Déscription : Calcul des propositions, raisonnement par réfutation, interprétation et sémantique, calcul des prédicats et déduction naturelle.

Conception objet en java

Maîtrise MASS · T.D.M. · (26h)

Responsable : J. Durand-Lose ([e-mail])

Déscription : Approfondissement des concepts objets et du langage Java (héritage, encapsulation, . . . ). Réalisation d’applications gérant l’accès aux bases de données

(JDBC). Construction des interfaces graphiques (swing).

Compilation, Analyse

Licence informatique · T.D.M. · (20h)

Responsable : O. Lecarme ([e-mail])

Déscription : Étude des grammaires LR(k), LL(k), LALR(1). Développement manuel d’analyseur lexical et syntaxique descendant. Utilisation de lex/yacc pour l’analyse lexical et syntaxique ascendante. Utilisation de bison pour la partie séman-tique.

Raisonnement automatique et preuve de programmes

Maîtrise informatique · Cours · (6h)

Déscription : Rappels de logique. Étude des méthodes de raisonnement pour la logique mathématique (réfutation, résolution et induction). Notions de systèmes de preuve automatiques et interactifs.

Détails ESSI – deuxième cycle

Bases de données relationnelles

2ème année · T.D.M. · (32h)

Responsable : M. Rueher ([e-mail])

Déscription : Étude du modèle relationnel (algèbre, formes normales). Utilisa-tion de langage SQL pour définir et manipuler les données. Définition des contraintes d’unicité, de référence ou d’intégrité. Développement d’un application web basée sur les JSP et JDBC pour accéder à un emploi du temps.

Concepts, langages et architectures du Web (2ème semestre)

2ème année · T.D.M. · (40h)

Responsable : P. Sander ([e-mail])

Déscription : L’ensemble du module est articulé autour de XML et de Java. Pilo-tage du développement des applications avec ANT. Définition du schéma de données persistantes à l’aide de JDO. Utilisation des définitions de schémas DTD et XSD.

Traitement des données XML à l’aide de SAX, JAXP et XSL(T).

Méthodes et techniques dans les applications relationnelles

3ème année et DESS · T.D.M. · (28h)

Responsable : A-M. Hugues ([e-mail])

Déscription : Les travaux dirigés du module portent sur le développement complet d’une application. Modélisation de la partie conception par des cas d’utilisation UML et des diagrammes ORM (Object Role Modeling). Gestion de la persistance à m’aide de la technologie EJB. Interface réalisée sous forme de pages HTML et JSP.

4

Encadrements – responsabilités collectives

• Rédaction de sujets de T.D. et T.P.,
• Rédaction, surveillance et corrections d’examens,
• Encadrement travaux d’étude, Licence informatique, 2002 et 2003 :

« Simulation de croissance d’arbres. »

• Encadrement travaux d’étude et de recherche, Maîtrise informatique, 2002 :

« Étude et interprétation d’un langage formel basé sur la réécriture. »

(R. Bertuli, J.-F. Dahan, S. Forget, M. Le Gleut)

5

Activités de Recherche

Mes travaux de recherches portent sur la preuve et la vérification de programmes.

Durant ma thèse de doctorat [8], mes recherches furent principalement orientées vers la théorie de l’induction mathématique. Je me suis aussi intéressé à ses applications pratiques dès mon stage de DEA et mes recherches actuelles portent principalement sur les systèmes d’édition collaboratifs.

• Induction mathématique 2

Un théorème inductif est une formule qui peut être démontrée à partir d’un en-semble d’axiomes. La démonstration utilise des règles d’inférences comme le modus ponens, l’instanciation de variables et le remplacement d’égaux par des égaux, ainsi qu’un principe de récurrence. Le problème général d’induction mathématique se for-mule comme suit :

• Données : un ensemble A d’axiomes de la forme C =⇒ l = r et une formule logique φ ;
• Question : est-ce que φ est un théorème inductif de A (c’est-à-dire est-ce que φ est valide dans le modèle initial de A) ?

L’objectif est ici le développement de méthodes capables d’effectuer de façon au-tomatique, et si possible efficace, le problème spécifié ci-dessus. L’induction mathé-matique est utilisée pour démontrer des conjectures de logique mathématique, mais elle a aussi des applications importantes et reconnues, tant en informatique fondamen-tale qu’en intelligence artificielle (vérification de programmes séquentiels et parallèles, analyse des spécifications, synthèse des programmes, systèmes experts, synthèse et vé-rification des composants électroniques, etc.).

Il existe de nombreux systèmes de preuves théoriques ou logiciels utilisant l’in-duction mathématique. Cependant, la preuve d’un théorème non-trivial requiert trop souvent une ou plusieurs interactions humaines. Ces interactions consistent en l’apport de lemmes, de généralisations ou de schéma d’induction. Notamment, aucun travail de recherche n’avait pu exposer une méthode correcte (non-heuristique) de généralisa-tion ; c’est-à-dire une méthode introduisant automatiquement une généralisation valide si et seulement si la conjecture est valide.

Notre approche est basée sur une analyse purement syntaxique des règles de réécri-tures non conditionnelles définissant les fonctions sur lesquelles porte une conjecture.

Cette étude nous à permis de comprendre la manière dont ces fonctions manipulent leurs arguments et comment les formes normales des instances closes d’un terme sont engendrées. Ainsi, nous pouvons identifier, dans les deux côtés d’une équation, des sous-termes identiques qui peuvent donc être remplacés par une variable sans que la validité de la conjecture n’en soit affectée. L’algorithme basé sur cette technique est la première méthode de généralisation correcte pour l’induction mathématique. Ce résul-tat a été présenté aux JFPLC’2002 [7] ainsi qu’à AFL’02 [3]. Un article sur ce sujet est en phase de corrections pour le journal Theoretical Computer Science (TCS).

Cette étude des formes normales nous a aussi permis de développer une nouvelle méthode pour prouver des théorèmes inductifs conceptuellement différente des ap-

2 Cette partie de mes recherches est décrite plus en profondeur dans le résumé de ma thèse :

http ://[lien]

6

proches existantes (induction implicite ou explicite, ou preuve par consistance). Cette méthode appelée « induction par partition de termes » à été présentée à RTA’03 [4].

• Vérification dans les systèmes collaboratifs

De nombreuses recherches (voir [Han94,LLR99,BMS+01] ont déjà traité de ma-nière formelle le domaine des systèmes temporels. Cependant les systèmes repartis et collaboratifs ont la particularité de confronter plusieurs systèmes temporels indé-pendant. Il existe donc des propriétés propres à la validation de tels systèmes qui ne peuvent être aisément prises en compte par ces recherches.

Les systèmes d’édition collaborative (ou groupware) permettent à plusieurs utili-sateurs de travailler en commun sur une même tâche. Pour gérer la concurrence entre deux actions portant sur une même partie de cette tâche, il existe deux solutions prin-cipales.

La première consiste à bloquer pour un des utilisateurs la ressource éditée. Cette solution, utilisée notamment pour les bases de données, augmente le temps de réponse du système et est donc peu adaptée à des applications temps-réel. Nous avons présenté à FLAIRS’99 [1] un heuristique de généralisation pour les théories conditionnelles. Puis nous avons appliqué cet heuristique aux preuves de contraintes d’intégrités de bases de données formalisées par le calcul de situation [McCH79]. Le calcul de situation est un formalisme permettant de représenter les systèmes temporels. L’état de la base de données est représenté par une situation qui est construite inductivement à partir des opération affectant la base. Ce résultat a été présenté à IEA/AIE-99 [2].

La deuxième solution consiste à répliquer pour chaque utilisateur les données édi-tées. Dans ce cas, les opérations effectuées par un utilisateur sont distribuées sur tous les autres sites. Si deux utilisateurs modifient au même moment une même donnée, un conflit apparaît. Pour résoudre ces conflits, l’approche transformationnelle [EG89]

propose de modifier les opérations distantes en fonction des opérations locales. Cepen-dant, pour vérifier que les différentes copies restent identiques après l’application des opérations locales et distantes, la fonction de transformation T doit satisfaire les deux conditions suivantes 3 [RNG96] :

C 1 : op 1 ◦ T (op 2 , op 1 ) ≡ op 2 ◦ T (op 1 , op 2 )

C 2 : T (op 3 , op 1 ◦ T (op 2 , op 1 )) = T (op 3 , op 2 ◦ T (op 1 , op 2 ))

La condition C 1 porte sur une équivalence sémantique. L’effet produit par le coté droit de l’égalité doit être le même que celui produit par le coté gauche. Par contre, la condition C 2 porte sur une égalité syntaxique entre les opérations produites par les transformations des deux cotés de l’équation. La condition C 2 est difficile à traiter

« manuellement » car le nombre de cas à traiter peut rapidement devenir très important, même pour des données « simples ». Par exemple, il y a 123 cas différents pour la preuve de C 2 sur des chaîne de caractères. Par contre, des techniques de réécriture par cas et de procédure de décision sont bien adaptées à ce type de preuve. Ainsi, un logiciel comme SPIKE, qui implémente ces techniques, peut traiter cette conjecture de manière automatique.

Pour vérifier C 1 une première idée peut être de représenter les données éditées par un type abstrait. Cependant, la structure des données éditées par le système peut

3 Toutes les formules présentées sont implicitement universellement quantifiées. L’opérateur ◦ représente une séquence d’opérations.

7

être complexe (e.g. un arbre XML). La preuve de la condition C 1 requière alors de nombreuses sous-preuves portant sur des propriétés de la structure des données. Notre idée est de capturer l’intuition du développeur de système lorsqu’il teste manuellement ses transformations. Pour cela, nous formalisons à l’aide du calcul de situation l’effet de chaque opération sur un ensemble de caractéristiques représentant l’état du système.

Chacune des caractéristiques dont le développeur souhaite vérifier la convergence est représentée par une fonction dont l’un des argument est l’état du système. Par exemple, pour les chaînes de caractères, la fonction carAt(n, st) a pour valeur le caractère à la n ième position dans l’état st. La propriété découlant de C 1 que l’on souhaite vérifier est donc :

C 1,carAt : carAt(n, do(st, op 1 ◦ T (op 2 , op 1 )))) = carAt(n, do(st, op 2 ◦ T (op 1 , op 2 )))

La fonction do(st, op) représente l’application d’une opération op (ou d’une séquence d’opérations) sur un état st du système.

L’outil VOTE (voir page 10) permet de tester automatiquement ces propriétés. L’uti-lisateur décrit la fonction de transformation et les fonctions représentant les caractéris-tiques du système à l’aide d’un mini-langage algorithmique. Ces définitions sont ré-écrites par VOTE en un ensemble de règle de réécritures conditionnelles. Le logiciel permet d’identifier des séquences d’opérations qui violent les conditions C 1,f et C 2 .

Ces séquences d’opérations sont retournées à l’utilisateur afin qu’il corrige sa fonction de transformation.

Ces recherches récentes vont être très prochainement publiées. En effet, deux pa-piers acceptés [5, 6] présentent ces travaux ainsi que l’environnement logiciel VOTE.

Des travaux futurs devraient combiner cette méthode aux preuves observationnelles

(appelées aussi hidden algebra) [GLR00,RB02]. Par essence, ces méthodes sont proches car elle propose aussi de spécifier le comportement des objets manipulés au lieu que leur implémentation interne. De plus, les preuves observationnelles ont montrée des ap-plications prometteuse dans la programmation orienté objet et la concurrence [GL01,GMK02].

• Visite

J’ai été accueilli à partir du 6 janvier 2003 au Loria (INRIA Lorraine) pour une période d’un mois par le projet CASSIS dirigé par M. Rusinowitch. J’y ai travaillé sur la vérification de la convergence dans les logiciels d’édition collaboratifs avec A. Imine et M. Rusinowitch de l’équipe CASSIS sur des problématiques proposé par l’équipe

ECOO.

Références bibliographiques

[BMS+01] · N. Bjorner, Z. Manna, H. Sipma and T. Uribe. Deductive Verification of

Real-time Systems using STeP. Theoretical Computer Science (253), pp.

27-60, 2001.

[EG89] · C.A. Ellis and S.J. Gibbs, Concurrency control in groupware systems,

SIGMOD Conference (18), pp. 399-407, 1989.

[GLR00] · J. Goguen, K. Lin and G. Rosu. Circular Coinductive Rewriting. In Pro-

ceedings of Automated Software Engineering, pp. 123-131, IEEE Press, 2000.

8

[GL01]

[GMK02]

[Han94]

[McCH69]

[RNG96]

[RB02]

J. Goguen and K. Lin. Web-based Support for Cooperative Software En-gineering. In Annals of Software Engineering (12), pp. 167-191, 2001.

J. Goguen, G. Malcolm and T. Kemp. A Hidden Herbrand Theorem :

Combining the Object, Logic and Functional Paradigms. In Journal of Logic and Algebraic Programming (51), pp. 1-41, 2002.

H. Hansson, Time and Probability in Formal Design of Distributed Sys-tems. Elsevier, 1994.

J. McCarthy and P. Hayes, Some philosophical problems from the stand-point of the artificial intelligence. In Machine Intelligence (4), pp. 463-

502, 1969.

M. Ressel, D. Nitsche-Ruhland and R. Gunzenhauser. An Integrating, Transformation-Oriented Approach to Concurrency Control and Undo in Group Editors. In Proceedings of the ACM Conference on Computer

Supported Cooperative Work (CSCW’96), pp. 288-297, 1996.

M. Rusinowitch and A. Bouhoula. Observational proofs by rewriting.

Theoretical Computer Science (275), pp. 675-698, 2002.

9

Logiciels

Ces deux logiciels sont disponibles à partir de l’adresse :

[lien]

• NICE (Nice Induction for Conditional Equations)

NICE est un logiciel de preuve automatique écrit en Java et muni d’une interface graphique. Ce logiciel est basé sur la logique du premier ordre et l’induction mathé-matique. NICE n’a pas pour vocation de concurrencer les logiciels équivalents – tel que SPIKE ou RRL – mais il m’a permis d’implanter les algorithmes présents dans ma thèse et de les tester sur des exemples non-triviaux. NICE est composé d’un analyseur syntaxique et sémantique, d’éditeurs graphiques spécifiques ainsi que d’une machinerie de preuve multi-thread.

• VOTE (Validation of Operational Transformation Environment)

VOTE est un environnent dédié à la vérification formelle des systèmes collaboratifs.

Cet environnement fonctionne en trois étapes.

• La première étape permet aux développeurs d’outils collaboratifs de définir algo- rithmiquement les transformations ainsi que les fonctions décrivant un système.

Ces définitions sont analysées, puis transformées en axiomes de la logique du premier ordre.

• La deuxième étape utilise directement le logiciel SPIKE pour vérifier les condi- tions de convergence à partir de ces axiomes.
• La troisième étape – écrite par A. Imine de l’équipe CASSIS du Loria en Perl – récupère, si besoin, les cas qui posent problème à SPIKE pour les soumettre à l’utilisateur.

VOTE en cours de développement depuis janvier 2003 (mais une première version est déjà totalement utilisable). La partie que j’ai personnellement développé (la pre-mière étape) est écrite en Java, une partie du code étant partagée avec NICE. Nous avons essayé de développer cet environnement en gardant à l’esprit que les utilisa-teurs finaux de cet outil ont peu de chance d’être spécialisés dans les systèmes de preuve. VOTE est utilisé depuis sa création par l’équipe ECOO du Loria (contact P.

Molli ([e-mail]) et G. Oster ([e-mail])).

10

Recommandation professionnelles

Des lettres de recommandations ont été demandées aux personnalités scientifiques suivantes. Ces personnes peuvent être contactées pour de plus amples informations.

• Professeur Emmanuel K OUNALIS (directeur de thèse).

Université de Nice – Sophia Antipolis, Laboratoire I3S, Dpt. Informatique, Parc Valrose,

[adresse] Cedex 2, FRANCE

Phone : ([téléphone]

Email : [e-mail]

• Professeur Michel R UEHER (responsable équipe COPRIN).

U.N.S.A., École Superieure en Sciences Informatiques

930, Route des Colles, BP 145

[adresse] Antipolis Cedex, FRANCE

Phone : ([téléphone]

Email : [e-mail]

• Michaël R USINOWITCH , directeur de recherche (rapporteur de thèse – res- ponsable équipe CASSIS).

LORIA

B.P. 239 - Campus Scientifique

[adresse] Cedex, FRANCE

Phone : ([téléphone]

Email : [e-mail]

• Professeur Claude G ODART (responsable équipe ECOO).

LORIA

B.P. 239 - Campus Scientifique

[adresse] Cedex, FRANCE

Phone : ([téléphone]

Email : [e-mail]

11

Publications

Les références ci-après sont disponibles à l’adresse internet :

[lien]

Actes de conférences internationales avec comité de lecture

[1] E. Kounalis et P. [nom]. Generalization discovery for proofs by induction in condi-tional theories. In Proceedings of Twelfth International FLAIRS Conference, pp.

250-256, Orlando, Floride, mai 1999. AAAI Press.

[2] E. Kounalis et P. [nom]. Mechanizing proofs of integrity constraints in the situation calculus. In Proceedings of Twelfth International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA/AIE), pp. 372-381, Cairo, Egypte, juin 1999. LNCS 1611, Springer.

[3] P. [nom] et E. Kounalis. Inductive Languages and Generalizations. In Proceedings of Tenth International Conference on Automata and Formal Languages (AFL), De-brecen, Hungary, août 2002. Publicationes Mathematicae.

[4] P. [nom] et E. Kounalis. “Term Partition” for Mathematical Induction. In Procee-dings of Fourteenth International Conference on Rewriting Techniques and Appli-cations (RTA), Valencia, Spain, juin 2003. LNCS 2706, Springer.

[5] A. Imine et P. [nom]. Automatic Detection of Copies Divergence in Collabora-tive Editing System. In Prooceedings of Eighth International Workshop on Formal

Methods for Industrial Critical Systems (FMICS), Trondheim, Norway, juin 2003.

ENTCS Series, Elsevier Science, to appear.

[6] A. Imine, P. Molli, G. Oster et P. [nom]. VOTE : Group Editors Analyzing Tool. In Prooceedings of Fourth International Workshop on First-Order Theorem Proving

(FTP), Valencia, Spain, juin 2003. ENTCS 86(1), Elsevier Science.

Actes de conférences francophones avec comité de lecture

[7] P. [nom] et E. Kounalis Généralisations correctes pour l’induction mathématique.

In Actes des Onzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes, pp. 211-226, Nice, France, mai 2002. Hermes

Science.

Autres

[8] Généralisations et méthodes correctes pour l’induction mathématique. Thèse de doctorat, Université de Nice – Sophia Antipolis, France, mars 2002.

[9] P. [nom] et E. Kounalis Sound generalizations in mathematical induction. Accepté

• sous conditions - à Theoretical Computer Science (TCS).

12