• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 75
  • 38
  • 19
  • Tagged with
  • 138
  • 65
  • 47
  • 37
  • 33
  • 32
  • 27
  • 24
  • 24
  • 22
  • 21
  • 18
  • 18
  • 17
  • 16
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
131

Neural Network Modeling for Prediction under Uncertainty in Energy System Applications. / Modélisation à base de réseaux de neurones dédiés à la prédiction sous incertitudes appliqué aux systèmes energétiques

Ak, Ronay 02 July 2014 (has links)
Cette thèse s’intéresse à la problématique de la prédiction dans le cadre du design de systèmes énergétiques et des problèmes d’opération, et en particulier, à l’évaluation de l’adéquation de systèmes de production d’énergie renouvelables. L’objectif général est de développer une approche empirique pour générer des prédictions avec les incertitudes associées. En ce qui concerne cette direction de la recherche, une approche non paramétrique et empirique pour estimer les intervalles de prédiction (PIs) basés sur les réseaux de neurones (NNs) a été développée, quantifiant l’incertitude dans les prédictions due à la variabilité des données d’entrée et du comportement du système (i.e. due au comportement stochastique des sources renouvelables et de la demande d'énergie électrique), et des erreurs liées aux approximations faites pour établir le modèle de prédiction. Une nouvelle méthode basée sur l'optimisation multi-objectif pour estimer les PIs basée sur les réseaux de neurones et optimale à la fois en termes de précision (probabilité de couverture) et d’information (largeur d’intervalle) est proposée. L’ensemble de NN individuels par deux nouvelles approches est enfin présenté comme un moyen d’augmenter la performance des modèles. Des applications sur des études de cas réels démontrent la puissance de la méthode développée. / This Ph.D. work addresses the problem of prediction within energy systems design and operation problems, and particularly the adequacy assessment of renewable power generation systems. The general aim is to develop an empirical modeling framework for providing predictions with the associated uncertainties. Along this research direction, a non-parametric, empirical approach to estimate neural network (NN)-based prediction intervals (PIs) has been developed, accounting for the uncertainty in the predictions due to the variability in the input data and the system behavior (e.g. due to the stochastic behavior of the renewable sources and of the energy demand by the loads), and to model approximation errors. A novel multi-objective framework for estimating NN-based PIs, optimal in terms of both accuracy (coverage probability) and informativeness (interval width) is proposed. Ensembling of individual NNs via two novel approaches is proposed as a way to increase the performance of the models. Applications on real case studies demonstrate the power of the proposed framework.
132

Contributions à la vérification formelle d'algorithmes arithmétiques

Martin-Dorel, Erik 26 September 2012 (has links) (PDF)
L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le "dilemme du fabricant de tables" (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'"approximation polynomiale rigoureuse", permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre "vérifieur ISValP" est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en "précision augmentée" pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de "double-arrondi", qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis.
133

Musique et langage: spécificités, interactions et associations spatiales / Music and language: specificities, interactions and spatial associations

Lidji, Pascale 30 April 2008 (has links)
L’objectif de ce travail était d’examiner la spécificité fonctionnelle du traitement et des représentations des hauteurs musicales. À cette fin, ce traitement a été comparé à celui des phonèmes de la parole, d’une part, et aux associations spatiales évoquées par des séquences ordonnées, d’autre part. Nos quatre études avaient pour point commun d’adapter à un nouvel objet de recherche des méthodes bien établies en psychologie cognitive. Ainsi, nous avons exploité la tâche de classification accélérée (Etude 1) de Garner (1974), l’analyse des conjonctions illusoires en mémoire (Etude 2), l’additivité de la composante mismatch negativity (MMN) des potentiels évoqués (Etude 3) et l’observation d’associations spatiales de codes de réponse (Etude 4).<p>Les trois premières études, menées chez des participants non-musiciens, portaient sur la spécificité de traitement des hauteurs par rapport à celui des phonèmes au sein de stimuli chantés. Les deux premières études ont mis en évidence un effet surprenant de la nature des phonèmes sur leurs interactions avec le traitement des mélodies :les voyelles apparaissaient plus intégrées à la mélodie que les consonnes. Ceci était vrai à la fois lors du traitement en temps réel de non-mots chantés (Etude 1) et au niveau des traces en mémoire de ces mêmes non-mots (Etude 2, utilisant une tâche de reconnaissance à choix forcé permettant la mise en évidence de conjonctions illusoires). Cette dissociation entre voyelles et consonnes quant à leur intégration avec les traitements mélodiques ne semblait pas causée par des caractéristiques acoustico-phonétiques telles que la sonorité. Les résultats de la troisième étude indiquaient que les MMNs en réponse à des déviations de hauteur et de voyelle n’étaient pas additives et que leur distribution topographique ne différait pas selon le type de déviation. Ceci suggère que, même au niveau pré-attentionnel, le traitement des voyelles n’est pas indépendant de celui des hauteurs. <p>Dans la quatrième étude, nous avons comparé le traitement des hauteurs musicales à un autre domaine :la cognition spatiale. Nous avons ainsi montré que les non-musiciens comme les musiciens associent les notes graves à la partie inférieure et les notes aiguës à la partie supérieure de l’espace. Les deux groupes liaient aussi les notes graves au côté gauche et les notes aiguës au côté droit, mais ce lien n’était automatique que chez les musiciens. Enfin, des stimuli musicaux plus complexes (intervalles mélodiques) n’évoquaient ces associations spatiales que chez les musiciens et ce, uniquement sur le plan horizontal.<p>Ces recherches contribuent de plusieurs manières à la compréhension de la cognition musicale. Premièrement, nous avons montré que les consonnes et les voyelles diffèrent dans leurs interactions avec la musique, une idée à mettre en perspective avec les rôles différents de ces phonèmes dans l’évolution du langage. Ensuite, les travaux sur les représentations spatiales des hauteurs musicales ouvrent la voie à un courant de recherche qui aidera à dévoiler les liens potentiels entre habiletés musicales et spatiales.<p>/<p>The purpose of this work was to examine the functional specificity of musical pitch processing and representation. To this aim, we compared musical pitch processing to (1) the phonological processing of speech and (2) the spatial associations evoked by ordered sequences. The four studies described here all use classical methods of cognitive psychology, which have been adapted to our research question. We have employed Garner’s (1974) speeded classification task (Study 1), the analysis of illusory conjunctions in memory (Study 2), the additivity of the mismatch negativity (MMN) component of event-related potentials (Study 3), as well as the observation of spatial associations of response codes (Study 4).<p>The three first studies examined, in non-musician participants, the specificity of pitch processing compared to phoneme processing in songs. Studies 1 and 2 revealed a surprising effect of phoneme category on their interactions with melodic processing: vowels were more integrated with melody than were consonants. This was true for both on-line processing of sung nonwords (Study 1) and for the memory traces of these nonwords (Study 2, using a forced-choice recognition task allowing the occurrence of illusory conjunctions). The difference between vowels and consonants was not due to acoustic-phonetic properties such as phoneme sonority. The results of the third study showed that the MMN in response to pitch and to vowel deviations was not additive and that its brain topography did not differ as a function of the kind of deviation. This suggests that vowel processing is not independent from pitch processing, even at the pre-attentive level.<p>In the fourth study, we compared pitch processing to another domain: spatial cognition. We showed that both musicians and non-musicians map pitch onto space, in that they associate low-pitched tones to the lower spatial field and high-pitched tones to the higher spatial field. Both groups of participants also associated low pitched-tones with the left and high-pitched tones with the right, but this association was automatic only in musicians. Finally, more complex musical stimuli such as melodic intervals evoked these spatial associations in the horizontal plane only in musicians.<p>This work contributes to the understanding of music cognition in several ways. First, we have shown that consonants and vowels differ in their interactions with music, an idea related to the contrasting roles of these phonemes in language evolution. Second, the work on the spatial representation of pitch opens the path to research that will help uncover the potential links between musical and spatial abilities.<p> / Doctorat en sciences psychologiques / info:eu-repo/semantics/nonPublished
134

GPU-enhanced power flow analysis / Calcul de Flux de Puissance amélioré grâce aux Processeurs Graphiques

Marin, Manuel 11 December 2015 (has links)
Cette thèse propose un large éventail d'approches afin d'améliorer différents aspects de l'analyse des flux de puissance avec comme fils conducteur l'utilisation du processeurs graphiques (GPU). Si les GPU ont rapidement prouvés leurs efficacités sur des applications régulières pour lesquelles le parallélisme de données était facilement exploitable, il en est tout autrement pour les applications dites irrégulières. Ceci est précisément le cas de la plupart des algorithmes d'analyse de flux de puissance. Pour ce travail, nous nous inscrivons dans cette problématique d'optimisation de l'analyse de flux de puissance à l'aide de coprocesseur de type GPU. L'intérêt est double. Il étend le domaine d'application des GPU à une nouvelle classe de problème et/ou d'algorithme en proposant des solutions originales. Il permet aussi à l'analyse des flux de puissance de rester pertinent dans un contexte de changements continus dans les systèmes énergétiques, et ainsi d'en faciliter leur évolution. Nos principales contributions liées à la programmation sur GPU sont: (i) l'analyse des différentes méthodes de parcours d'arbre pour apporter une réponse au problème de la régularité par rapport à l'équilibrage de charge ; (ii) l'analyse de l'impact du format de représentation sur la performance des implémentations d'arithmétique floue. Nos contributions à l'analyse des flux de puissance sont les suivantes: (ii) une nouvelle méthode pour l'évaluation de l'incertitude dans l'analyse des flux de puissance ; (ii) une nouvelle méthode de point fixe pour l'analyse des flux de puissance, problème que l'on qualifie d'intrinsèquement parallèle. / This thesis addresses the utilization of Graphics Processing Units (GPUs) for improving the Power Flow (PF) analysis of modern power systems. Currently, GPUs are challenged by applications exhibiting an irregular computational pattern, as is the case of most known methods for PF analysis. At the same time, the PF analysis needs to be improved in order to cope with new requirements of efficiency and accuracy coming from the Smart Grid concept. The relevance of GPU-enhanced PF analysis is twofold. On one hand, it expands the application domain of GPU to a new class of problems. On the other hand, it consistently increases the computational capacity available for power system operation and design. The present work attempts to achieve that in two complementary ways: (i) by developing novel GPU programming strategies for available PF algorithms, and (ii) by proposing novel PF analysis methods that can exploit the numerous features present in GPU architectures. Specific contributions on GPU computing include: (i) a comparison of two programming paradigms, namely regularity and load-balancing, for implementing the so-called treefix operations; (ii) a study of the impact of the representation format over performance and accuracy, for fuzzy interval algebraic operations; and (iii) the utilization of architecture-specific design, as a novel strategy to improve performance scalability of applications. Contributions on PF analysis include: (i) the design and evaluation of a novel method for the uncertainty assessment, based on the fuzzy interval approach; and (ii) the development of an intrinsically parallel method for PF analysis, which is not affected by the Amdahl's law.
135

Modeling sea-level rise uncertainties for coastal defence adaptation using belief functions / Utilisation des fonctions de croyance pour la modélisation des incertitudes dans les projections de l'élévation du niveau marin pour l'adaptation côtière

Ben Abdallah, Nadia 12 March 2014 (has links)
L’adaptation côtière est un impératif pour faire face à l’élévation du niveau marin,conséquence directe du réchauffement climatique. Cependant, la mise en place d’actions et de stratégies est souvent entravée par la présence de diverses et importantes incertitudes lors de l’estimation des aléas et risques futurs. Ces incertitudes peuvent être dues à une connaissance limitée (de l’élévation du niveau marin futur par exemple) ou à la variabilité naturelle de certaines variables (les conditions de mer extrêmes). La prise en compte des incertitudes dans la chaîne d’évaluation des risques est essentielle pour une adaptation efficace.L’objectif de ce travail est de proposer une méthodologie pour la quantification des incertitudes basée sur les fonctions de croyance – un formalisme de l’incertain plus flexible que les probabilités. Les fonctions de croyance nous permettent de décrire plus fidèlement l’information incomplète fournie par des experts (quantiles,intervalles, etc.), et de combiner différentes sources d’information. L’information statistique peut quand à elle être décrite par de fonctions des croyance définies à partir de la fonction de vraisemblance. Pour la propagation d’incertitudes, nous exploitons l’équivalence mathématique entre fonctions de croyance et intervalles aléatoires, et procédons par échantillonnage Monte Carlo. La méthodologie est appliquée dans l’estimation des projections de la remontée du niveau marin global à la fin du siècle issues de la modélisation physique, d’élicitation d’avis d’experts, et de modèle semi-empirique. Ensuite, dans une étude de cas, nous évaluons l’impact du changement climatique sur les conditions de mers extrêmes et évaluons le renforcement nécessaire d’une structure afin de maintenir son niveau de performance fonctionnelle. / Coastal adaptation is an imperative to deal with the elevation of the global sealevel caused by the ongoing global warming. However, when defining adaptationactions, coastal engineers encounter substantial uncertainties in the assessment of future hazards and risks. These uncertainties may stem from a limited knowledge (e.g., about the magnitude of the future sea-level rise) or from the natural variabilityof some quantities (e.g., extreme sea conditions). A proper consideration of these uncertainties is of principal concern for efficient design and adaptation.The objective of this work is to propose a methodology for uncertainty analysis based on the theory of belief functions – an uncertainty formalism that offers greater features to handle both aleatory and epistemic uncertainties than probabilities.In particular, it allows to represent more faithfully experts’ incomplete knowledge (quantiles, intervals, etc.) and to combine multi-sources evidence taking into account their dependences and reliabilities. Statistical evidence can be modeledby like lihood-based belief functions, which are simply the translation of some inference principles in evidential terms. By exploiting the mathematical equivalence between belief functions and random intervals, uncertainty can be propagated through models by Monte Carlo simulations. We use this method to quantify uncertainty in future projections of the elevation of the global sea level by 2100 and evaluate its impact on some coastal risk indicators used in coastal design. Sea-level rise projections are derived from physical modelling, expert elicitation, and historical sea-level measurements. Then, within a methodologically-oriented case study,we assess the impact of climate change on extreme sea conditions and evaluate there inforcement of a typical coastal defence asset so that its functional performance is maintained.
136

Nouvelle méthodologie générique permettant d’obtenir la probabilité de détection (POD) robuste en service avec couplage expérimental et numérique du contrôle non destructif (CND) / New generic methodology to obtain robust In-Service Probability Of Detection (POD) coupling experimental and numerical simulation of Non-Destructive Test (NDT)

Reseco Bato, Miguel 17 May 2019 (has links)
L’évaluation des performances des procédures de Contrôle Non Destructifs (CND) en aéronautique est une étape clé dans l’établissement du dossier de certification de l’avion. Une telle démonstration de performances est faite à travers l’établissement de probabilités de détection (Probability Of Detection – POD), qui intègrent l’ensemble des facteurs influents et sources d’incertitudes inhérents à la mise en œuvre de la procédure. Ces études, basées sur des estimations statistiques faites sur un ensemble représentatif d’échantillons, reposent sur la réalisation d’un grand nombre d’essais expérimentaux (un minimum de 60 échantillons contenant des défauts de différentes tailles, qui doivent être inspectés par au moins 3 opérateurs [1]), afin de recueillir un échantillon suffisant pour une estimation statistique pertinente. Le coût financier associé est élevé, parfois prohibitif, et correspond majoritairement à la mise en œuvre des maquettes servant aux essais. Des travaux récents [2-5] ont fait émerger une approche de détermination de courbes POD utilisant la simulation des CND, notamment avec le logiciel CIVA. L’approche, dite de propagation d’incertitudes, consiste à : - Définir une configuration nominale d’inspection, - Identifier l’ensemble des paramètres influents susceptibles de varier dans l’application de la procédure, - Caractériser les incertitudes liées à ces paramètres par des lois de probabilités, - Réaliser un grand nombre de simulations par tirage aléatoire des valeurs prises par les paramètres variables selon les lois de probabilités définies. Le résultat de cet ensemble de simulations constitue enfin la base de données utilisée pour l’estimation des POD. Cette approche réduit de façon très importante les coûts d’obtention des POD mais est encore aujourd’hui sujette à discussions sur sa robustesse vis-à-vis des données d’entrée (les lois de probabilité des paramètres incertains) et sur la prise en compte des facteurs humains. L’objectif de cette thèse est de valider cette approche sur des cas d’application AIRBUS et d’en améliorer la robustesse afin de la rendre couramment utilisable au niveau industriel, notamment en la faisant accepter par les autorités de vol (FAA et EASA). Pour ce faire le thésard devra mener des campagnes de validations des codes de simulation des CND, mettre en œuvre la méthodologie décrite plus haut sur les cas d’application AIRBUS, puis proposer et mettre en œuvre des stratégies d’amélioration de la robustesse de la méthode vis-à-vis des données d’entrée et des facteurs liés à l’humain. / The performance assessment of non-destructive testing (NDT) procedures in aeronautics is a key step in the preparation of the aircraft's certification document. Such a demonstration of performance is done through the establishment of Probability of Detection (POD) laws integrating all sources of uncertainty inherent in the implementation of the procedure. These uncertainties are due to human and environmental factors in In-Service maintenance tasks. To establish experimentally these POD curves, it is necessary to have data from a wide range of operator skills, defect types and locations, material types, test protocols, etc. Obtaining these data evidences high costs and significant delays for the aircraft manufacturer. The scope of this thesis is to define a robust methodology of building POD from numerical modeling. The POD robustness is ensured by the integration of the uncertainties through statistical distributions issued from experimental data or engineering judgments. Applications are provided on titanium beta using high frequency eddy currents NDT technique. First, an experimental database will be created from three environments: laboratory, A321 aircraft and A400M aicraft. A representative sample of operators, with different certification levels in NDT technique, will be employed. Multiple inspection scenarios will be carried out to analyze these human and environmental factors. In addition, this study will take into account the impact of using different equipments in the HFEC test. This database is used, subsequently, to build statistical distributions. These distributions are the input data of the simulation models of the inspection. These simulations are implemented with the CIVA software. A POD module, based on the Monte Carlo method, is integrated into this software. This module will be applied to address human and ergonomic influences on POD. Additionally this module will help us to understand in a better way the equipment impact in POD curves. Finally, the POD model will be compared and validated with the experimental results developed.
137

Modèles réduits pour des analyses paramètriques du flambement de structures : application à la fabrication additive / Reduced order models for multiparametric analyses of buckling problems : application to additive manufacturing

Doan, Van Tu 06 July 2018 (has links)
Le développement de la fabrication additive permet d'élaborer des pièces de forme extrêmement complexes, en particulier des structures alvéolaires ou "lattices", où l'allégement est recherché. Toutefois, cette technologie, en très forte croissance dans de nombreux secteurs d'activités, n'est pas encore totalement mature, ce qui ne facilite pas les corrélations entre les mesures expérimentales et les simulations déterministes. Afin de prendre en compte les variations de comportement, les approches multiparamétriques sont, de nos jours, des solutions pour tendre vers des conceptions fiables et robustes. L'objectif de cette thèse est d'intégrer des incertitudes matérielles et géométriques, quantifiées expérimentalement, dans des analyses de flambement. Pour y parvenir, nous avons, dans un premier temps, évalué différentes méthodes de substitution, basées sur des régressions et corrélations, et différentes réductions de modèles afin de réduire les temps de calcul prohibitifs. Les projections utilisent des modes issus soit de la décomposition orthogonale aux valeurs propres, soit de développements homotopiques ou encore des développements de Taylor. Dans un second temps, le modèle mathématique, ainsi créé, est exploité dans des analyses ensemblistes et probabilistes pour estimer les évolutions de la charge critique de flambement de structures lattices. / The development of additive manufacturing allows structures with highly complex shapes to be produced. Complex lattice shapes are particularly interesting in the context of lightweight structures. However, although the use of this technology is growing in numerous engineering domains, this one is not enough matured and the correlations between the experimental data and deterministic simulations are not obvious. To take into account observed variations of behavior, multiparametric approaches are nowadays efficient solutions to tend to robust and reliable designs. The aim of this thesis is to integrate material and geometric uncertainty, experimentally quantified, in buckling analyses. To achieve this objective, different surrogate models, based on regression and correlation techniques as well as different reduced order models have been first evaluated to reduce the prohibitive computational time. The selected projections rely on modes calculated either from Proper Orthogonal Decomposition, from homotopy developments or from Taylor series expansion. Second, the proposed mathematical model is integrated in fuzzy and probabilistic analyses to estimate the evolution of the critical buckling load for lattice structures.
138

Contributions à la vérification formelle d'algorithmes arithmétiques / Contributions to the Formal Verification of Arithmetic Algorithms

Martin-Dorel, Erik 26 September 2012 (has links)
L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le «dilemme du fabricant de tables» (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'«approximation polynomiale rigoureuse», permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre «vérifieur ISValP» est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en «précision augmentée» pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de «double-arrondi», qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis. / The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the ``Table Maker's Dilemma'' (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of ``Rigorous Polynomial Approximation'', allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel's lemma that we have formalized for both univariate and bivariate cases. In particular, our ``ISValP verifier'' is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of ``augmented-precision'' FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the ``double-rounding'' phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.

Page generated in 0.1087 seconds