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.

Cette thèse présente la nouvelle implémentation de la Verified Polyhedra Library (VPL), une bibliothèque efficace de calcul polyédral.Elle fournit des opérateurs certifiés en Coq, s'appliquant sur des représentations en contraintes.La version précédente souffrait d'inefficacité lors d'opérateurs cruciaux, à savoir l'élimination de variables et l'enveloppe convexe.Dans ce document, je présente des améliorations importantes qui bénéficient à la modularité, la simplicité et au passage à l'échelle de la bibliothèque:le processus de certification est généralisé et simplifié;les conditions polynomiales sont maintenant traitées;Les calculs qui n'impliquent pas de certification sont effectués en flottant;de nouveaux algorithmes sont fournis pour la minimisation de représentation et la détection d'égalités implicites.D'un côté, l'implémentation d'un solveur de problèmes de Programmation Linéaire Paramétrique (PLP) a mené à une meilleure efficacité tant en nombre de contraintes que de générateurs.L'élimination de variables et l'enveloppe convexe sont tous deux encodés en problème PLP.Le PLP est un outil générique possédant de nombreuses applications, et qui permet d'éviter la génération de redondances grâce à l'utilisation d'une contrainte de normalisation.De plus, nous proposons de nouveaux opérateurs pour la gestion des contraintes polynomiales, l'un d'entre eux étant également encodé en tant que problème PLP.De l'autre, la certification de la bibliothèque a été grandement optimisée et simplifiée.La VPL suit un paradigme de vérification a posteriori, où les calculs non triviaux sont effectués par des oracles externes générant des témoins de correction.Ces témoins sont ensuite validés par un vérifieur écrit en Coq.Grâce à un cadre de certification puissant et innovant, le Polymorphic Factory Style (PFS), la plupart des aspects délicats de la génération de témoins sont maintenant évitée.La souplesse du PFS est démontrée par la création d'une tactique en COQ qui découvre les égalités implicites en arithmétique linéaire. / This thesis presents the design and implementation of the Verified Polyhedra Library (VPL), a scalable library for polyhedral calculus.It provides Coq-certified polyhedral operators that work on constraints-only representation.The previous version was inefficient on crucial operations, namely variable elimination and convex hull.In this work, I present major improvements that have been made in scalability, modularity and simplicity:The certification process is generalized and simplified;Polynomial guards can now be handled;Computations that do not involve certification use floating-points;New algorithms are presented for minimization and detection of implicit equalities.On the one hand, the implementation of a solver for Parametric Linear Programming (PLP) problems led to an improved scalability both in dimension and in number of constraints.Variable elimination and convex hull are now encoded as such.PLP is a generic tool that has many applications, and that avoids generating redundancies thanks to a normalization constraint.Additionally, we provide new operators for handling multivariate polynomials, one of which being also encoded as a PLP problem.On the other hand, the certification part of the library has been greatly optimized and simplified.The VPL follows a result-verification paradigm, where complex computations are performed by untrusted oracles that generate witnesses of correctness, themselves validated by a certified Coq checker.Thanks to an innovative and powerful certification framework known as Polymorphic Factory Style (PFS), most cumbersome parts of the witness generation are now avoided.The flexibility of PFS is attested by the creation of a Coq tactic for learning equalities in linear arithmetic.

Dans les réacteurs à Eau Pressurisée (REP), les pastilles d’uranium sont isolées de l’eau du circuit primaire par des gaines en alliages de zirconium (Zy-4, M5, ZIRLO). Ces gaines jouent un rôle crucial en termes de sureté car elles sont la première barrière de confinement des produits de fission. En conditions nominales d’utilisation, la corrosion des gaines induite par l’environnement du circuit primaire (320 °C, 155 bars, présence de lithium et de bore) se traduit par l’oxydation du zirconium et la formation de phases fragiles d’hydrures de zirconium sous l’interface oxyde/métal. Ces phénomènes couplés affectent la tenue mécanique de la gaine et, in fine, limitent la durée de vie des assemblages combustibles en réacteur (~ 5 ans). Ce travail vise à mieux comprendre le phénomène de corrosion des alliages de zirconium.Dans un premier temps, une modélisation par éléments finis de la diffusion-corrosion du Zircaloy-4 a été réalisée pour simuler la cinétique d’oxydation observée expérimentalement. Le modèle analytique de Wagner prédit une évolution de l’épaisseur d’oxyde proportionnelle à la racine carrée du temps (régime parabolique). En pratique, la cinétique d’oxydation du Zircaloy-4 en autoclave s’écarte de la loi parabolique et est quasiment cubique. Plusieurs phénomènes sont susceptibles d’expliquer cette différence entre la cinétique expérimentale et le modèle analytique, notamment la présence de fortes contraintes de compression au sein de la couche d’oxyde. La prise en compte dans la modélisation de l’effet des contraintes sur la diffusion de l’oxygène permet de simuler et d’expliquer cet écart à la loi parabolique.Dans un second temps, nous avons simulé par éléments finis la diffusion de l’oxygène à travers une couche polycristalline de zircone. Les grains de zircone sont modélisés par un agrégat de polyèdres de Voronoï. Un espace entre les polyèdres est également maillé pour modéliser les joints de grains. Ces échantillons numériques ont été utilisés pour étudier l’effet de la microstructure et de la microtexture des couches de zircone sur la diffusion de l'oxygène. Les simulations sont nourries par les données expérimentales obtenues sur des lames minces de zircone formées sur Zircaloy-4 et hydrure de zirconium. / In Pressurized Water Reactor (PWR), zirconium-based alloy cladding tubes are immersed in high pressure water containing boron (1000 wt. boron) and lithium (2 wt. ppm) at high temperature (320 °C). The corrosion induced by this environment is mainly due to the oxidation of the zirconium which transforms in zirconia. This phenomenon is one of the limiting factors of the in-pile fuel rod lifetime (~ 5 years). Therefore, it is important to predict the corrosion process of zirconium based alloys in PWR conditions. Zirconium-based alloys oxidation is sub-parabolic inlike the Wagner theory which predicts a parabolic kinetics. Two finite element models were developed to simulate this phenomenon : the diffuse interface model and the sharp interface model. Both simulate parabolic oxidation kinetics. The growth stress effects on oxygen diffusion were studied to explain the gap between theory and experience. Taking into account the influence of the hydrostatic stress and its gradient into the oxygen flux expression, sub-parabolic oxidation kinetics were simulated. The sub-parabolic behavior of the oxidation kinetics can be explained by a non-uniform compressive stress level into the oxide layer. Simulations of oxygen diffusion throught polycristalline layer of zirconia were performed. Zirconia grains are modelled by Voronoï tesselation and a space between grains is meshed to model grain boundaries. These numerical samples are used to study the effect of zirconia microstructure and microtexture on oxygen diffusion. Experimental data from thin foils of zirconia formed on Zircaloy-4 and zirconium hydrure are used in the simulations.

.

Etant donné trois entiers k, s et a, nous prouvons dans le premier chapitre qu'il existe un graphe k-régulier fini (resp. un graphe k-régulier connexe fini) dont le groupe d'automorphismes a exactement s orbites sur l'ensemble des sommets et a orbites sur l'ensemble des arêtes si et seulement si<p><p>(s,a)=(1,0) si k=0,<p>(s,a)=(1,1) si k=1,<p>s=a>0 si k=2,<p>0< s <= 2a <= 2ks si k>2.<p><p>(resp.<p>(s,a)=(1,0) si k=0,<p>(s,a)=(1,1) si k=1 ou 2,<p>s-1<=a<=(k-1)s+1 et s,a>0 si k>2.)<p><p>Nous étudions les polyèdres convexes de R³ dans le second chapitre. Pour tout polyèdre convexe P, nous notons Isom(P) l'ensemble des isométries de R³ laissant P invariant. Si G est un sous-groupe de Isom(P), le f_G-vecteur de P est le triple d'entiers (s,a,f) tel que G ait exactement s orbites sur l'ensemble sommets de P, a orbites sur l'ensemble des arêtes de P et f orbites sur l'ensemble des faces de P. Remarquons que (s,a,f) est le f_{id}-vecteur (appelé f-vecteur dans la littérature) d'un polyèdre si ce dernier possède exactement s sommets, a arêtes et f faces. Nous généralisons un théorème de Steinitz décrivant tous les f-vecteurs possibles. Pour tout groupe fini G d'isométries de R³, nous déterminons l'ensemble des triples (s,a,f) pour lesquels il existe un polyèdre convexe ayant (s,a,f) comme f_G-vecteur. Ces résultats nous permettent de caractériser les triples (s,a,f) pour lesquels il existe un polyèdre convexe tel que Isom(P) a s orbites sur l'ensemble des sommets, a orbites sur l'ensemble des arêtes et f orbites sur l'ensemble des faces.<p><p>La structure d'incidence I(P) associée à un polyèdre P consiste en la donnée de l'ensemble des sommets de P, l'ensemble des arêtes de P, l'ensemble des faces de P et de l'inclusion entre ces différents éléments (la notion de distance ne se trouve pas dans I(P)). Nous déterminons également l'ensemble des triples d'entiers (s,a,f) pour lesquels il existe une structure d'incidence I(P) associée à un polyèdre P dont le groupe d'automorphismes a exactement s orbites de sommets, a orbites d'arêtes et f orbites de sommets. / Doctorat en sciences, Spécialisation mathématiques / info:eu-repo/semantics/nonPublished

Étant donné un graphe G = (V U T, E), tel que V U T représente l'ensemble des sommets où T est un ensemble de terminaux, et une fonction poids w associée aux sommets non terminaux, le problème du séparateur de poids minimum consiste à partitionner V U T en k + 1 sous-ensembles {S, V1,..., Vk} tel qu'il n'y a aucune arête entre deux sous-ensembles différents Vi et Vj, chaque Vi contient exactement un terminal et le poids de S est minimum. Dans cette thèse, nous étudions le problème d'un point de vue polyèdral. Nous donnons deux formulations en nombres entiers pour le problème, et pour une de ces formulations, nous étudions le polyèdre associé. Nous présentons plusieurs inégalités valides, et décrivons des conditions de facette. En utilisant ces résultats, nous développons un algorithme de coupes et branchement pour le problème. Nous étudions également le polytope des séparateurs dans les graphes décomposables par sommets d'articulation. Si G est un graphe qui se décompose en G1 et G2, alors nous montrons que le polytope des séparateurs dans G peut être décrit à partir de deux systèmes linéaires liés à G1 et G2. Ceci donne lieu à une technique permettant de caractériser le polytope des séparateurs dans les graphes qui sont récursivement décomposables. Ensuite, nous étudions des formulations étendues pour le problème et proposons des algorithmes de génération de colonnes et branchement ainsi que des algorithmes de génération de colonnes, de coupes et branchement. Pour chaque formulation, nous présentons un algorithme de génération de colonnes, une procedure pour le calcul de la borne duale ainsi qu'une règle de branchement. De plus, nous présentons quatre variantes du problème du séparateur. Nous montrons que celles-ci sont NP-difficiles, et pour chacune d'elles nous donnons une formulation en nombres entiers et présentons certaines classes d'inégalités valides. / Given a graph G = (V U T, E) with V U T the set of vertices, where T is a set of terminals, and a weight function w, associated with the nonterminal nodes, the multi-terminal vertex separator problem consists in partitioning V U T into k + 1 subsets {S, V1,..., Vk} such that there is no edge between two different subsets Vi and Vj, each Vi contains exactly one terminal and the weight of S is minimum. In this thesis, we consider the problem from a polyhedral point of view. We give two integer programming formulations for the problem, for one of them, we investigate the related polyhedron. We describe some valid inequalities and characterize when these inequalities define facets. Using these results, we develop a Branch-and-Cut algorithm for the problem. We also study the multi-terminal vertex separator polytope in the graphs decomposable by one node cutsets. If G is a graph that decomposes into G1 and G2, we show that the multi-terminal vertex separator polytope in G can be described from two linear systems related to G1 and G2. This gives rise to a technique for characterizing the multi-terminal vertex separator polytope in the graphs that are recursively decomposable. Moreover, we propose three extended formulations for the problem and derive Branch-and-Price and Branch-and-Cut-and-Price algorithms. For each formulation we present a column generation scheme, the way to compute the dual bound, and the branching scheme. Finally, we discuss four variants of the multi-terminal vertex separator problem. We show that all these variants are NP-hard and for each one we give an integer programming formulation and present some class of valid inequalities.

Les méthodes par éléments discrets constituent une alternative par rapport aux méthodes<br />par éléments finis pour la modélisation du comportement d'un milieu divisé : sol, milieux<br />granulaires, etc . Dans ce mémoire l'objectif est d'étudier un matériau granulaire soumis à des sollicitations<br />cycliques : le ballast des voies ferrées soumis au passage des trains. Nous présentons à la<br />suite d'une étude bibliographique sur le comportement du ballast, la méthode de résolution NonSmooth<br />Contact Dynamics, et nous exposons l'ensemble des développements nécessaires dans le<br />cas bidimensionnel et tridimensionnel : un algorithme de détection entre polygones et entre polyèdres<br />convexes, le paramétrage, la résolution du problème de contact frottant. Nous déterminons<br />ensuite les paramètres optimaux pour des simulations de chargement cyclique. Dans une dernière<br />partie, nous présentons ensuite un ensemble de résultats montrant l'aptitude des méthodes par éléments<br />discrets à décrire l'évolution d'un massif granulaire sous chargement cyclique. L'analyse<br />d'une comparaison entre une expérience et la simulation met évidence le comportement particulier<br />de ce type de système, qui s'assimile à une couche mince granulaire où des micro-structures particulières<br />guident la réponse mécanique du milieu. Dans le cas tridimensionnel, des comportements<br />mécaniques connus ont été retrouvés, à titre d'exemple, en analysant l'évolution de structures<br />maçonnées. Nous présentons une étude de la résistance latérale de la voie ballastée, en considérant<br />des formes de grains issues de la digitalisation de grains réels, pour laquelle on retrouve un<br />comportement identifié expérimentalement.

Notre laboratoire travaille sur la conception et le développement de Modules de Contrôle et d'Interface pour la Téléopération (MCIT). Le but de MCIT est de fournir à l'opérateur une aide pour la perception et pour la commande du site téléopéré. L'aide visuelle consiste en la mise à jour et la superposition de la BD3D sur l'image vidéo. Afin d'automatiser cette aide, un système de reconnaissance de polyèdres à partir d'une image de luminance a été développé et intégré à MCIT dans le cadre de cette thèse. Ce système est constitué d'un module de traitement d'images et d'un module d'appariement 2D/3D. Le 1er module est basé sur la modélisation orientée objet. La transformée de Hough, dont une amélioration est apportée, est utilisée pour extraire les segments de droite de l'image. L'organisation perceptive est appliquée pour trouver un modèle 2D de l'image. Le 2nd module est constitué de deux étapes. La 1ère étape concerne la prédiction d'hypothèses, elle utilise 2 méthodes d'appariement : la méthode des graphes qui donne un nombre d'hypothèses très réduit grâce à l'utilisation des invariants topologiques et projectifs mais, elle échoue en présence de défauts du traitement d'images. Dans ce cas, nous appliquons la méthode du hachage géométrique qui donne toujours une solution. Deux méthodes d'extraction de graphes d'aspects applicables aux polyèdres ont été également développées. La première est destinée à l'appariement par graphes, la seconde est utilisée par le hachage géométrique. La 2nde étape concerne la vérification de l'appariement, nous avons mis en oeuvre des méthodes existantes de recalage et avons développé une méthode hybride qui donne une meilleure précision. Le développement de la calibration automatique de la caméra à l'aide d'un robot a permis également d'augmenter la précision et l'autonomie du système.

Dans ce mémoire, on se propose de décrire certains résultats de l'auteur sur les propriétés $p$-adiques des fonctions $L$ associées à des caractères sur les corps finis, à la suite des travaux de Dwork, Robba, Adolphson et Sperber, Wan, entre autres. On parlera aussi de sommes de caractères (et de leurs fonctions $L$) définies sur certains anneaux locaux.

Cette thèse porte sur la modélisation morphologique de matériaux cimentaires, et sur l'analyse de leurs propriétés linéaires élastiques. Dans cet objectif, des images 3D, obtenues par micro-tomographie, de matériaux cimentaires (mortier et béton) sont étudiées. Dans un premier temps, l'image de mortier est segmentée afin d'obtenir une image de microstructure réelle pour des calculs en élasticité linéaire. L'image de béton est utilisée, après traitement, pour la détermination des caractéristiques morphologiques du matériau. Un modèle aléatoire de béton est ensuite développé et validé par des données morphologiques. Ce modèle comporte trois phases qui correspondent à la matrice, les granulats et les pores. La phase des granulats est modélisée par implantation sans recouvrement de polyèdres de Poisson. Pour cela, un algorithme de génération vectorielle de polyèdres de Poisson est mis en place et validé par des mesures morphologiques. Enfin, les propriétés linéaires élastiques effectives de la microstructure de mortier et de microstructures simulées sont déterminées par méthode FFT (Fast-Fourier Transform), pour différents contrastes entre le module de Young des granulats et de la matrice. Cette étude des propriétés effectives est complétée par une analyse locale des champs dans la matrice, afin de déterminer l'arrangement spatial entre les zones de concentration de contraintes dans la matrice, et les différentes phases de la microstructure (granulats et pores). Une caractérisation statistique des champs est de plus réalisée, avec notamment le calcul du Volume Élémentaire Représentatif (VER). Une comparaison des propriétés élastiques effectives et locales obtenues d'une part sur une microstructure simulée contenant des polyèdres et d'autre part sur une microstructure contenant des sphères est de plus effectuée. / The goal of this thesis is to develop morphological models of cementitious materials and use these models to study their local and effective response. To this aim, 3D images of cementitious materials (mortar and concrete), obtained by micro-tomography, are studied. First, the mortar image is segmented in order to obtain an image of a real microstructure, to be used for linear elasticity computations. The image of concrete is used, after being processed, to determine various morphological characteristics of the material. A random model of concrete is then developed and validated by means of morphological data. This model is made up of three phases, corresponding to the matrix, aggregates and voids. The aggregates phase is modelled by implantation of Poisson polyhedra without overlap. For this purpose, an algorithm suited to the vector generation of Poisson polyhedra is introduced and validated with morphological measurements. Finally, the effective linear elastic properties of the mortar and other simulated microstructures are estimated with the FFT (Fast-Fourier Transform) method, for various contrasts between the aggregates and matrix' Young moduli. To complete this work, focused on effective properties, an analysis of the local elastic response in the matrix phase is undertaken, in order to determine the spatial arrangement between stress concentration zones in the matrix and the phases of the microstructure (aggregates and voids). Moreover, a statistical fields characterization, in the matrix, is achieved, including the determination of the Representative Volume Element (RVE) size. Furthermore, a comparison between effective and local elastic properties obtained from microstructures containing polyhedra and spheres is carried out.