Cette thèse est une contribution à la théorie des modèles des corps valués. Les principaux résultats de ce texte sont des résultats d’éliminations des quantificateurs et des imaginaires. Le premier chapitre contient une étude des imaginaires dans les extensions finies de Qp. On y démontre que ces corps ainsi que leurs ultraproduits éliminent les imaginaires dans le langage géométrique. On en déduit un résultat de rationalité uniforme pour les fonctions zêta associées aux familles de relations d’équivalences définissables dans les extensions finies de Qp. La motivation première du deuxième chapitre est l’étude de W(F_p^alg) en tant que corps valué analytique de différence. Plus généralement, on démontre un théorème d’élimination des quantificateurs de corps dans le langage RV pour les corps valués analytiques -Henséliens de caractéristique nulle. On donne aussi une axiomatisation de la théorie de W(F_p^alg) ainsi qu’une preuve qu’elle est NIP. Dans le troisième chapitre, on prouve la densité des types définissables dans certains enrichissements d’ACVF. On en déduit un critère pour l’élimination des imaginaires et la propriété d’extension invariante. Ce chapitre contient aussi des résultats abstraits sur les ensembles extérieurement définissables dans les théories NIP. Dans le dernier chapitre, les résultats du chapitre précédent sont appliqués à VDF, la modèle complétion des corps valués munis d’une dérivation qui préserve la valuation, pour obtenir l’élimination des imaginaires dans le langage géométrique ainsi que la densité des types définissables et la propriété d’extension invariante. Ce chapitre contient aussi des considérations sur les fonctions définissables, les types et les groupes définissables dans VDF. / This thesis is about the model theory of valued fields. The main results in this text are eliminationsof quantifiers and imaginaries. The first chapter is concerned with imaginaries in finite extensions of Qp. I show that these fields and their ultraproducts eliminate imaginaries in the geometric language. As a corollary, I obtain the uniform rationality of zeta functions associated to families of equivalence relations that aredefinable in finite extensions of Qp.The motivation for the second chapter is to study W(F_p^alg) as an analytic difference valued field. More generally, I show a field quantifier elimination theorem in the RV-language for -Henselian characteristic zero valued fields with an analytic structure. I also axiomatise the theory of W(F_p^alg) and I show that this theory is NIP.In the third chapter, I prove the density of definable types in certain enrichments of ACVF. From this result, I deduce a criterion for the elimination of imaginaries and the invariant property. This chapter also contains abstract results on externally definable sets in NIP theories. In the last chapter, the previous chapter is applied to VDF, the model completion of valued fields with a valuation preserving derivation, to obtain the elimination of imaginaries in the geometric language, as well as the density of definable types and the invariant extension property. This chapter also contains considerations about definable functions, types and definable groupes in VDF.

Les structures o-minimales, introduites dans les années '80 par Van den Dries et largement étudiées par Wilkie et Macintyre répondent à Grothendick en donnant le cadre d'une géométrie modérée. <br /> <br />Cette thèse montre un théorème du complémentaire explicite pour les<br />structures o-minimales polynomialement bornées, ce qui équivault à la modèle-complétude en théorie des modèles.<br /><br />En 1968, Gabrielov montre un théorème du complémentaire pour<br />les sous-analytiques globaux, qui en implique la o-minimalité. Il améliore ce résultat en 96, avec un théorème explicite. Une généralisation de celui-ci est présentée ici.<br /><br />Par des arguments de valuation dus à Lojaciewicz et à Miller, des propriétés de quasi-analycité sont exhibées, qui permettent d'adapter le schéma classique des preuves de modèle-complétude. Ce résultat permet de mieux comprendre la façon dont sont générées les structures o-minimales et donne un langage réduit sur lequel une structure polynomialement bornée est modèle-complète.

Il est important que les logiciels pilotant les systèmes critiques (avions, centrales nucléaires, etc.) fonctionnent correctement — alors que la plupart des systèmes informatisés de la vie courante (micro-ordinateur, distributeur de billets, téléphone portable) ont des dysfonctionnements visibles. Il ne s'agit pas là d'un simple problème d'ingéniérie : on sait depuis les travaux de Turing et de Cook que la preuve de propriétés de bon fonctionnement sur les programmes est un problème intrinsèquement difficile.<br /><br />Pour résoudre ce problème , il faut des méthodes à la fois efficaces (coûts en temps et en mémoire modérés), sûres (qui trouvent tous les problèmes possibles) et précises (qui fournissent peu d'avertissements pour des problèmes inexistants). La recherche de ce compromis nécessite des recherches faisant appel à des domaines aussi divers que la logique formelle, l'analyse numérique ou l'algorithmique « classique ».<br /><br />De 2002 à 2007 j'ai participé au développement de l'outil d'analyse statique Astrée. Ceci m'a suggéré quelques développements annexes, à la fois théoriques et pratiques (utilisation de techniques de preuve formelle, analyse de filtres numériques...). Plus récemment, je me suis intéressé à l'analyse modulaire de propriétés numériques et aux applications en analyse de programme de techniques de résolution sous contrainte (programmation semidéfinie, techniques SAT et SAT modulo théorie).

Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. / This work studies the verification of software components in avionics critical embedded systems. As the failure of suchsystems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification.Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if itdoes not. Current methods are unable to handle the verification problems stemming from realistic systems. Discoveringadditional information (invariants) on the system can however restrict the search space enough to strengthen the proofobjective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariantdiscovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic forthe generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convexhull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives correspondingto safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude currenttechniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that itscales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecturewe propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and ageneralisation to Property Directed Reachability to linear real arithmetic and integer octagons.

Un problème de géométrie algébrique réelle s'exprime sous forme d’un système d’équations et d’inéquations polynomiales, dont l’ensemble des solutions est un ensemble semi-algébrique. L'objectif de cette thèse est de montrer comment les algorithmes de ce domaine peuvent être décrits formellement dans le langage du système de preuve Coq.Un premier résultat est la définition formelle et la certification de l’algorithme de transformation de Newton présentée dans la thèse d'A. Bostan. Ce travail fait intervenir non seulement des polynômes, mais également des séries formelles tronquées. Un deuxième résultat est la description d'un type de donnée représentant les ensembles semi-algébriques. Un ensemble semialgébrique est représenté par une formule logique du premier ordre basée sur des comparaisons entre expressions polynomiales multivariées. Pour ce type de données, nous montrons comment obtenir les différentes opérations ensemblistes et allons jusqu'à décrire les fonctions semi-algébriques. Pour toutes ces étapes, nous fournissons des preuves formelles vérifiées à l'aide de Coq. Enfin, nous montrons également comment la continuité des fonctions semi-algébrique peut être décrite, mais sans en fournir une preuve formelle complète. / A real algebraic geometry problem is expressed as a system of polynomial equations and inequalities, and the set of solutions are semi-algebraic sets. The objective of this thesis is to show how the algorithms of this domain can be formally described in the language of the Coq proof system. A first result is the formal definition and certification of the Newton transformation algorithm presented in A. Bostan's thesis. This work involves not only polynomials, but also truncated formal series. A second result is the description of a data type representing semi-algebraic sets. A semi-algebraic set is represented by a first-order logical formula based on comparisons between multivariate polynomial expressions. For this type of data, we show how to obtain the different set operations all the way to describing semialgebraic functions. For all these steps, we provide formal proofs verified with Coq. Finally, we also show how the continuity of semi-algebraic functions can be described, but without providing a fully formalized proof.