Cette Habilitation à Diriger des Recherches est le fruit des résultats, tant en recherche qu'en enseignement ou en transfert, de mon activité d'enseignant chercheur. Initiée au sein du Laboratoire d'Informatique, de Microélectronique et de Robotique de Montpellier (LIRMM, UMR CNRS/UM2) de 1991 à 1994, cette activité s'est ensuite concrétisée au sein du Laboratoire de Génie Informatique et d'Ingénierie de Production (LGI2P) de l'Ecole des Mines d'Alès où j'exerce depuis 1994.<br />Le travail de recherche entrepris depuis le début du Doctorat en 1991 relève de la thématique de la modélisation de systèmes complexes puis de la vérification et de la validation de ces modèles. Ceci a pour objectif d'assurer, ou à défaut de rassurer, le modeleur sur la qualité des modèles, sur leur pertinence vis-à-vis du système considéré et sur le respect d'exigences qui ont présidé à leur construction. La recherche a donc consisté au développement d'approches de modélisation, de spécification formelle de propriétés, de vérification par preuve de propriétés au moyen de Graphes Conceptuels et de simulation comportementale. Les domaines d'application privilégiés ont été les systèmes de contrôle commande répartis, puis plus largement la modélisation d'entreprise et tentent aujourd'hui d'intégrer une dimension risque dans la modélisation d'entreprise et de s'ouvrir plus largement à l'ingénierie des systèmes complexes. Les résultats sont des langages et un cadre de modélisation intégré, un langage de spécification baptisé LUSP, une suite de mécanismes de preuve formelle et de simulation qui ont donné lieu à divers encadrements de thèses, de travaux et à des transferts vers l'industrie. <br />Enfin, l'activité d'enseignement a tenté de rester cohérente avec le profil de compétence à la fois de producticien et d'ingénierie système acquis ou inspiré par la thématique de recherche. Elle s'est déroulée dans le cadre de diverses Universités, Ecoles d'Ingénieurs ou de cursus spécialisés. Les résultats sont des propositions et l'accompagnement de thématiques nouvelles, une activité d'ingénierie pédagogique et une implication dans diverses responsabilités administratives.

De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Cette thèse revisite de deux manières le domaine abstrait des polyèdres utilisé pour l'analyse statique de programmes.D'abord, elle montre comment utiliser l'assistant à la preuve Coq pour apporter des garanties sur la correction des opérations sur les polyèdres sans compromettre l'efficacité de l'outil VP Lissu de ces travaux.L'outil est fondé sur le principe de la vérification de résultats :un oracle, auquel on ne fait pas confiance, fait les calculs,puis les résultats sont vérifiés par un validateur dont la correction est prouvée avec Coq. De plus, l'oracle fournit des témoins de la correction des résultats afin d'accélérer la vérification.L'autre caractéristique de VPL est l' utilsation de la seule représentation par contraintes des polyèdres,par opposition à l'approche habituelle qui consiste à utiliser à la fois des contraintes et des générateurs.Malgré ce choix inhabituel,les performances de VPL s'avèrent compétitives.Comme on pouvait le prévoir,l'opérateur "join",qui calcule l'enveloppe convexe de deux polyèdres,est le plus coûteux.Puisqu'il nécessite un grand nombre de projections,cette thèse explore plusieurs nouvelles approches de l'opérateur de projection,basées sur la programmation linéaire paramétrique.Elle propose une synthèse des variantes et des combinaisons possibles.La thèse se termine sur les éléments clés d'un nouvel algorithme de résolution tirant parti des spécificités de l'encodage afin d'obtenir de bonnes performances. / The work reported in this thesis revisits in two waysthe abstract domain of polyhedraused for static analysis of programs.First, strong guarantees are provided on the soundness of the operationson polyhedra,by using of the Coq proof assistant to check the soundness proofs.The means used to ensure correctnessdon't hinder the performance of the resultingVerimag Polyhedra Library (VPL).It is built on the principle of result verification:computations are performed by an untrusted oracleand their results are verified by a checkerwhose correctness is proved in Coq.In order to make verification cheap,the oracle computes soundness witnesses along with the results.The other distinguishing feature of VPL is thatit relies only on the constraint representation of polyhedra,as opposed to the common practice of using both constraints and generators.Despite this unusual choice,VPL turns out to be a competitive abstract domain of polyhedra,performance-wise.As expected, the join operator of VPL,which performs the convex hull of two polyhedra,is the costliest operator.Since it builds on the projection operator,this thesis also investigates a new approach toperforming projections,based on parametric linear programming.A new understanding of projection encoded asa parametric linear problem is presented.The thesis closes on a progress report in the design of a new solvingalgorithm,tailored to the specifics of the encodingso as to achieve good performance.

L'analyse réelle a de nombreuses applications car c'est un outil approprié pour modéliser de nombreux phénomènes physiques et socio-économiques. En tant que tel, sa formalisation dans des systèmes de preuve formelle est justifié pour permettre aux utilisateurs de vérifier formellement des théorèmes mathématiques et l'exactitude de systèmes critiques. La bibliothèque standard de Coq dispose d'une axiomatisation des nombres réels et d'une bibliothèque de théorèmes d'analyse réelle. Malheureusement, cette bibliothèque souffre de nombreuses lacunes. Par exemple, les définitions des intégrales et des dérivées sont basées sur les types dépendants, ce qui les rend difficiles à utiliser dans la pratique. Cette thèse décrit d'abord l'état de l'art des différentes bibliothèques d'analyse réelle disponibles dans les assistants de preuve. Pour pallier les insuffisances de la bibliothèque standard de Coq, nous avons conçu une bibliothèque facile à utiliser : Coquelicot. Une façon plus facile d'écrire les formules et les théorèmes a été mise en place en utilisant des fonctions totales à la place des types dépendants pour écrire les limites, dérivées, intégrales et séries entières. Pour faciliter l'utilisation, la bibliothèque dispose d'un ensemble complet de théorèmes couvrant ces notions, mais aussi quelques extensions comme les intégrales à paramètres et les comportements asymptotiques. En plus, une hiérarchie algébrique permet d'appliquer certains théorèmes dans un cadre plus générique comme les nombres complexes pour les matrices. Coquelicot est une extension conservative de l'analyse classique de la bibliothèque standard de Coq et nous avons démontré les théorèmes de correspondance entre les deux formalisations. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur une épreuve du Baccalauréat, pour les définitions et les propriétés des fonctions de Bessel ainsi que pour la solution de l'équation des ondes en dimension 1. / Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals and asymptotic behaviors. Moreover, an algebraic hierarchy makes it possible to apply some of the theorems in a more generic setting, such as complex numbers or matrices. Coquelicot is a conservative extension of the classical analysis of Coq's standard library and we provide correspondence theorems between the two formalizations. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation.

Nous avons commencé la thèse par la littérature d'enquête sur les approches SPLE et CbyC dans l'état de l'art. Sur la base de l'aperçu et des connaissances obtenues, nous avons analysé les problèmes existants et suggéré des moyens de les résoudre pour notre objectif principal. Nous avons proposé dans le chapitre 2 une méthodologie pour développer des lignes de produits afin que les produits générés soient corrects par construction. Notre intention principale est qu'un utilisateur n'a pas besoin de connaître le processus de génération de produit mais peut recevoir un produit final correct en sélectionnant une configuration de fonctionnalité. En utilisant la méthodologie, les produits finaux sont générés automatiquement et leur exactitude est garantie. À la suite de cette proposition, nous sommes passés au chapitre 3 pour définir la langue de FFML qui est utilisé pour l'écriture de modules. Le mécanisme de réutilisation et de modification, défini pour la langue et appliqué à toutes sortes d'artefacts (spécification, code et preuve de précision) réduit l'effort de programmation. Au chapitre 4, nous nous sommes concentrés sur la définition des mécanismes de composition pour la composition des modules FFML et les intégrons à l'outil FFML Product Generator. L'évaluation de notre méthodologie est réalisée par le développement de deux lignes de produits logiciels, le compte bancaire SPL et le SPL de poker, ce dernier étant un peu plus complexe que le premier. Dans l'évaluation, nous avons souligné les avantages et la limitation de notre méthodologie. / We began the thesis by survey literature on SPLE and CbyC approaches in the State of the Art. Based on the overview and the insights obtained, we have analyzed the existing problems and suggested ways to solve them for our main goal. We have proposed in Chapter 2 a methodology to develop product lines such that the generated products are correct-by-construction. Our main intention is that a user does not need to know the product generation process but can receive a correct final product from selecting a configuration of features. Using the methodology, the final products are generated automatically and their correctness is guaranteed. Following this proposal, we have moved in Chapter 3 to define the FFML language that is used for writing modules. The reuse and modification mechanism, defined for the language and applied to all kinds of artifacts (specification, code and correctness proof), reduce the programming effort. In Chapter 4, we have focused on defining the composition mechanisms for composing FFML modules and embedded them into the FFML Product Generator tool. The evaluation of our methodology is performed through the development of two software product lines, the Bank Account SPL and the Poker SPL, the latter being a bit more complex than the former. In the evaluation, we have highlighted the advantages and the limitation of our methodology.

L'objet de cette thèse est d'étudier les capacités du système Coq à mélanger démonstrations et programmes en pratique en essayant d'y implémenter une part du programme Kenzo, un outil de calcul formel en algèbre homologique. À cet effet, nous travaillons sous trois contrainte: nous voulons essayer de lire le programme comme une démonstration avec un contenu calculatoire, ces démonstrations doivent calculer efficacement et nous cherchons à éviter de dupliquer des morceaux de démonstration. Nous montrons dans un premier temps comment le soucis d'efficacité conduit à reconsidérer certains aspects des mathématiques traditionnelle. Nous proposons une abstraction catégorielle adaptée, qui répond à la fois à un soucis de clareté et au besoin de partager les démonstration quand c'est possible. Cette abstraction, bien que différente des propositions traditionnelles, permet de formuler les notions d'algèbre homologique dans un style proche de celui de Kenzo. Nous proposons par ailleurs des modifications au programme de Coq pour rendre les démonstrations plus confortables, et pour permettre d'écrire des programmes plus efficaces. La première modification permet d'utiliser des tactiques plus fines, souvent nécessaire quand l'utilisation des types dépendents se fait commune. La seconde permet d'utiliser les capacité du processeur pour faire des calculs plus efficaces sur des entiers. Pour finir nous proposons quelques pistes pour améliorer le partage et la clareté du code. Malheureusement, nous nous heurtons aux limites du système. Nous montrons ainsi que Coq ne tiens pas forcément ses promesses et qu'il y aura besoin de travaux théoriques pour comprendre comment lever ces limites.

CertiCrypt est une bibliothèque qui permet de vérifier la sécurité exacte de primitives cryptographiques dans l'assistant à la preuve Coq. CertiCrypt instrumente l'approche des preuves par jeux, et repose sur de nombreux domaines comme les probabilités, la complexité, l'algèbre, la sémantique des langages de programmation, et les optimisations de programmes. Dans cette thèse, nous présentons deux exemples d'utilisation d'EasyCrypt: le schéma d'encryption Hashed ElGamal, et les protocoles à connaissance nulle. Ces exemples, ainsi que les travaux antérieurs sur CertiCrypt, démontrent qu'il est possible de formaliser des preuves complexes; toutefois, l'utilisation de CertiCrypt demande une bonne expertise en Coq, et demeure laborieuse. Afin de faciliter l'adoption des preuves formelles par la communauté cryptographique, nous avons développé EasyCrypt, un outil semi-automatique capable de reconstruire des preuves formelles de sécurité à partir d'une ébauche formelle de preuve. EasyCrypt utilise des outils de preuves automatiques pour vérifier les ébauches de preuves, puis les compiles vers des preuves vérifiables avec CertiCrypt. Nous validons EasyCrypt en prouvant à nouveau Hashed ElGamal, et comparons cette nouvelle preuve avec celle en CertiCrypt. Nous prouvons également le schéma d'encryption Cramer-Shoup. Enfin, nous expliquerons comment étendre le langage de CertiCrypt à des classes de complexité implicite, permettant de modéliser la notion de fonctions en temps polynomial.

Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.

Ces dernières années ont vu l'émergence d'assistants interactifs de preuves riches en fonctionnalités et d'une grande maturité d'implémentation, ce qui a permis l'essor des grosses formalisations de résultats papier et la résolution de conjectures célèbres. Mais autant d'assistants de preuves reposent sur presque autant de logiques comme fondements théoriques. Cousineau et Dowek (2007) proposent le λΠ-calcul modulo comme un cadre universel cible pour tous ces environnement de démonstration. Nous montrons dans cette thèse comment ce formalisme particulièrement simple admet une implémentation d'un vérificateur de taille modeste mais pour autant modulaire et efficace, à la correction de laquelle on peut réduire la cohérence de systèmes tout entiers. <p> Un nombre croissant de preuves dépendent de calculs intensifs comme dans la preuve du théorème des quatre couleurs de Gonthier (2007). Les méthodologies telles que SSReflect et les outils attenants privilégient les preuves contenant de nombreux petits calculs plutôt que les preuves purement déductives. L'encodage de preuves provenant d'autres systèmes dans le λΠ-calcul modulo introduit d'autres calculs encore. Nous montrons comment gérer la taille de ces calculs en interprétant les preuves tout entières comme des programmes fonctionnels, que l'on peut compiler vers du code machine à l'aide de compilateurs standards et clé-en-main. Nous employons pour cela une variante non typée de la normalisation par évaluation (NbE), et montrons comment optimiser de précédentes formulation de celle-ci. <p> Au travers d'une seule petite modification à l'interprétation des termes de preuves, nous arrivons aussi à une représentation des preuves en syntaxe abstraite d'ordre supérieur (HOAS), qui admet naturellement un algorithme de typage sans aucun contexte de typage explicite. Nous généralisons cet algorithme à tous les systèmes de types purs (PTS). Nous observons que cet algorithme est une extension à un cadre avec types dépendants de l'algorithme de typage des assistants de preuves de la famille HOL. Cette observation nous amène à développer une architecture à la LCF pour une large classe de PTS, c'est à dire une architecture où tous les termes de preuves sont corrects par construction, a priori donc, et n'ont ainsi pas besoin d'être vérifié a posteriori. Nous prouvons formellement en Coq un théorème de correspondance entre les système de types sans contexte et leur pendant standard avec contexte explicite. Ces travaux jettent un pont entre deux lignées historiques d'assistants de preuves : la lignée issue de LCF à qui nous empruntons l'architecture du noyau, et celle issue de Automath, dont nous héritons la notion de types dépendants. <p> Les algorithmes présentés dans cette thèse sont au coeur d'un nouveau vérificateur de preuves appelé Dedukti et ont aussi été transférés vers un système plus mature : Coq. En collaboration avec Dénès, nous montrons comment étendre la NbE non typée pour gérer la syntaxe et les règles de réduction du calcul des constructions inductives (CIC). En collaboration avec Burel, nous généralisons des travaux précédents de Cousineau et Dowek (2007) sur l'encodage dans le λΠ-calcul modulo d'une large classe de PTS à des PTS avec types inductifs, motifs de filtrage et opérateurs de point fixe.

Cette recherche étudie l'enseignement des premiers éléments de l'Analyse réelle à la transition lycée/université à travers un modèle de variables macro-didactiques (VMD) relatives aux niveaux de formalisation et de familiarité des savoirs mathématiques proposés aux élèves. Lorsque l'on passe du lycée à l'université, les valeurs de ces variables sont dichotomiques et témoignent d'une profonde mutation dans le travail mathématique demandé. Nous nous posons la question des moyens que peut se donner l'enseignement des mathématiques, à l'entrée à l'université, pour gérer des variations aussi importantes et permettre aux étudiants d'accéder aux objets de l'Analyse réelle. <br />Une ingénierie a porté sur la construction et l'expérimentation, dans le cadre de la TSD (Théorie des Situations Didactiques), de deux situations sur les limites, que nous avons expérimentées à un niveau du cursus où seule l'existence formelle des objets de l'Analyse réelle a été établie par les professeurs. Nous avons ciblé le travail des étudiants sur les méthodes d'approximation, afin de favoriser des allers/retours entre les "preuves pragmatiques" géométriques ou numériques et l'utilisation des théorèmes d'Analyse. Les situations prennent en compte la dialectique sémantique/ syntaxique dans un processus de preuve, et permettent un retour efficace sur les savoirs visés. L'entrée dans un processus de preuves mixtes – pragmatiques vs formelles – a ainsi été rendu obligatoire dans le travail des étudiants, à travers l'émergence du problème général de l'existence et de l'accessibilité des nombres, des limites et des suites. <br />En conclusion, nous proposons de poursuivre l'étude du milieu théorique des situations de l'Analyse réelle, d'introduire d'autres situations expérimentales et d'étudier plus en profondeur les connaissances des étudiants dans le contrat didactique instauré par de telles situations.