Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions.

Nous nous intéressons dans cette thèse au model-checking des systèmes infinis, notamment<br />les systèmes paramétrés et les programmes récursifs parallèles. Nous présen\-tons un cadre<br />uniforme pour la vérification algorithmique de ces systèmes. Ce cadre est basé sur la <br />représentation des ensembles de configurations par des automates de mots ou d'arbres, et la<br />représentation des relations de transition des systèmes par des règles de réécritures de mots<br />ou de termes. Le problème de la vérification est ensuite réduit au calcul des ensembles des<br />accessibles dans ce cadre. Les contributions de cette thèse sont les suivantes:<br /><br />1- Définition d'une technique d'accélération générale. Nous proposons une méthode basée sur <br />des techniques d'extrapolation sur les automates, et nous étudions la puissance de cette approche.<br />2- Techniques de model-checking régulier pour la vérification des réseaux paramétrés avec des <br />topologies linéaires et arborescentes. En particulier, nous considérons les réseaux modélisés <br />par des systèmes de réécriture comprenant des semi-commutations, c-à-d. des règles de la forme ab -> ba,<br />et nous exhibons une classe de langages qui est effectivement fermée par ces systèmes.<br />3- Modélisation et vérification des programmes récursifs parallèles. Dans un premier temps, <br />nous étudions les modèles PRS qui sont plus généraux que les systèmes à pile, les réseaux de Petri,<br />et les systèmes PA; et nous proposons des algorithmes qui calculent les ensembles des accessibles <br />de (sous-classes de) PRS en considérant différentes sémantiques. <br /><br />Dans une autre approche, nous considérons des modèles basés sur des automates à pile communicants<br />et des systèmes de réécritures à-la CCS, et nous proposons des méthodes de vérification de ces modèles<br />basées sur le calcul d'abstractions des langages des chemins d'exécutions. Nous proposons un cadre<br />algébrique générique permettant le calcul de ces abstractions.

La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données. / This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications.

Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions. / This thesis comes within the domain of proofs of programs by deductive verification. The deductive verification generates from a program source and its specification a mathematical formula whose validity proves that the program follows its specification. The program source describes what the program does and its specification represents what the program should do. The validity of the formula is mainly verified by automatic provers. During the last ten years separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques.This thesis introduces a technique to express ideas from separation logic in the traditional framework of deductive verification. Unfortunately the mathematical formulas produced are not in the same first-order logic than the ones of provers. Thus this work defines new conversions between the polymorphic first-order logic and the many-sorted logic used by most proves.The first part of this thesis leads to an implementation in the Jessietool. The second part results in an important participation to the writing of the Why3 tool, in particular in the architecture and writing of the transformations which implement these conversions.