Présentation d'une approche déductive basée sur l'instantiation progressive de schémas de programmes fonctionnels. Un système formel de preuve est décrit dans lequel le lien entre schémas de programmes et schémas de propriétés est exhibe. La complétude relative et la correction de ce système sont prouvées notamment pour les fonctions partiellement définies. Des stratégies, guidées par l'utilisateur, sont ensuite proposées qui permettent de caractériser les propriétés nécessaires, propres à chaque schema, en termes de recherche de préconditions

.

.

Les règles de transformation des problèmes equationnels sont donnes permettant, en particulier, de décider de l'existence d'une solution fermée. Comme première application, il est montre comment calculer une grammaire pour le langage des termes fermes irréductibles par un système de réécriture. D'autres applications et extensions sont ensuite envisagées. En particulier, en programmation logique et dans les spécifications algébriques

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks.

L'analyse statique des programmes permet d'étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l'exécution d'un programme ne peut pas produire d'erreurs. Ces outils d'analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroître la confiance que l'on peut accorder aux résultats d'une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l'implantation d'un tel analyseur statique. En particulier, nous construisons au moyen de l'assistant à la preuve Coq des interpréteurs abstraits et prouvons qu'ils sont corrects ; c'est-à-dire nous établissons formellement que le résultat de l'analyse d'un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s'intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d'un programme sont aussi valides pour la version compilée de ce programme. Nous nous concentrons sur l'analyse de programmes écrits dans des langages de bas niveau. C'est-à-dire des langages qui ne fournissent que peu d'abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d'un analyseur qui ne peut pas s'appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu'un programme écrit en C (où l'arithmétique de pointeurs est omniprésente) ne peut pas produire d'erreurs à l'exécution. / Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error.

Avec la généralisation d'Internet, l'usage des protocoles cryptographiques est devenu omniprésent. Étant donné leur complexité et leur l'aspect critique, une vérification formelle des protocoles cryptographiques est nécessaire.Deux principaux modèles existent pour prouver les protocoles. Le modèle symbolique définit les capacités de l'attaquant comme un ensemble fixe de règles, tandis que le modèle calculatoire interdit seulement a l'attaquant derésoudre certain problèmes difficiles. Le modèle symbolique est très abstrait et permet généralement d'automatiser les preuves, tandis que le modèle calculatoire fournit des garanties plus fortes.Le fossé entre les garanties offertes par ces deux modèles est dû au fait que le modèle symbolique décrit les capacités de l'adversaire alors que le modèle calculatoire décrit ses limitations. En 2012 Bana et Comon ont proposé unnouveau modèle symbolique dans lequel les limitations de l'attaquant sont axiomatisées. De plus, si la sémantique calculatoire des axiomes découle des hypothèses cryptographiques, la sécurité dans ce modèle symbolique fournit desgaranties calculatoires.L'automatisation des preuves dans ce nouveau modèle (et l'élaboration d'axiomes suffisamment généraux pour prouver un grand nombre de protocoles) est une question laissée ouverte par l'article de Bana et Comon. Dans cette thèse nous proposons une procédure de décision efficace pour une large classe d'axiomes. De plus nous avons implémenté cette procédure dans un outil (SCARY). Nos résultats expérimentaux montrent que nos axiomes modélisant la sécurité du chiffrement sont suffisamment généraux pour prouver une large classe de protocoles. / With the rise of the Internet the use of cryptographic protocols became ubiquitous. Considering the criticality and complexity of these protocols, there is an important need of formal verification.In order to obtain formal proofs of cryptographic protocols, two main attacker models exist: the symbolic model and the computational model. The symbolic model defines the attacker capabilities as a fixed set of rules. On the other hand, the computational model describes only the attacker's limitations by stating that it may break some hard problems. While the former is quiteabstract and convenient for automating proofs the later offers much stronger guarantees.There is a gap between the guarantees offered by these two models due to the fact the symbolic model defines what the adversary may do while the computational model describes what it may not do. In 2012 Bana and Comon devised a new symbolic model in which the attacker's limitations are axiomatised. In addition provided that the (computational semantics) of the axioms follows from the cryptographic hypotheses, proving security in this symbolic model yields security in the computational model.The possibility of automating proofs in this model (and finding axioms general enough to prove a large class of protocols) was left open in the original paper. In this thesis we provide with an efficient decision procedure for a general class of axioms. In addition we propose a tool (SCARY) implementing this decision procedure. Experimental results of our tool shows that the axioms we designed for modelling security of encryption are general enough to prove a large class of protocols.

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks. / Term schematisations allow one to represent infinite sets of terms having a similar structure by a finite and compact form. In this work we study some issues related to the use of term schematisation in automated deduction, in particular in saturation-based first-order theorem proving. After a brief comparative study of existing schematisation formalisms, we focus on terms with integer exponents (or I-terms). We first propose a new approach allowing to automatically detect regularities (obviously not always) on search spaces. This is motivated by our aim at extending current theorem provers with qualitative improvements. For instance, detecting regularities permits to discover lemmata which is mandatory for terminating in some kinds of inductive proofs. We present DS3, a tool which implements these ideas. Our approach departs from existing techniques since on one hand it is completely independent of the proof procedure used and on the other hand it uses inductive generalization techniques instead of deductive ones. We discuss advantages and disadvantages of our method and we give some informal elements of comparison with similar approaches. Next we tackle some theoretical aspects of the use of I-terms in automated deduction. We prove that the direct extension of the ordered resolution calculus is refutationally complete. We provide an example showing that a direct extension of the superposition calculus is not refutationally complete and we propose a new inference rule to restore refutational completeness. We then propose an indexing algorithm for (a subclass of) I-terms. This algorithm is an extension of the perfect discrimination trees that are are employed by many efficient theorem provers to implement redundancy elimination rules. Finally we present DEI, a theorem prover with built-in capabilities to handle formulae containing I-terms. This theorem-prover is an extension of the E-prover developed by S. Schulz. We evaluate the performances of this software on a set of benchmarks.

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS / This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

Ce travail se situe dans le cadre des systèmes informatiques pour l'enseignement intégrant des capacités de raisonnement. Les exigences de ces EIAO (Environnement Interactif d'Apprentissage avec Ordinateur) sont à la fois d'ordre didactique et d'ordre informatique : exigence d'un contrat didactique à la sémantique claire et pré­cise; exigence d'une liberté maximale donnée à l'enseignant dans la formulation de ce contrat; exigence de capacités de déduction complètes; exigence de performances garantissant un niveau d'interactivité suffisant. Concrétement, nous avons conçu et réalisé le système TALC (Tuteur d'Aide Logique à la Construction) pour l'enseignement de la géométrie, dont l'objectif est de diagnostiquer la correction de la construction d'un apprenant vis-à-vis de la spécification d'une figure donnée par un enseignant. La définition du contrat didactique constitue le point central de notre travail. Notre point de vue est que son expression à l'aide de la logique du premier ordre est nécessaire à la fois pour obtenir une définition claire et pour fournir de bonnes explications à l'apprenant. Nous donnons ainsi une sémantique précise aux langages manipulés par le système : le langage logique LDL - à partir duquel est déterminé le diagnostic - et les langages d'interface. Nous présentons aussi les principes de la formulation de la théorie logique représentant les connaissances présupposées de l'élève. Nous établissons, par étapes de dérivation successives, l'expression logique de la correction d'une construction. Cette attitude est fructueuse. Elle nous a amenés à proposer le concept d'extension logique d'une formule par rapport à une autre, nécessaire pour prendre en compte des objets non décrits dans la spécification. Les perspectives ouvertes sont les suivantes : amélioration de la formulation du contrat didactique (par une meilleure définition de la négation), extension des langages d'interface, constitution de séquences didactiques, construction d'un modèle de l'apprenant à l'aide de techniques d'apprentissage et définition d'un langage d'expression des dialogues à tenir.