Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Sorted by: relevance · author · university · dateNew search

You searched for +publisher:"Université Paris-Sud – Paris XI" +contributor:("Boldo, Sylvie"). Showing records 1 – 2 of 2 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


Université Paris-Sud – Paris XI

1. Lelay, Catherine. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis.

Degree: Docteur es, Informatique, 2015, Université Paris-Sud – Paris XI

L'analyse réelle a de nombreuses applications car c'est un outil approprié pour modéliser de nombreux phénomènes physiques et socio-économiques. En tant que tel, sa formalisation dans des systèmes de preuve formelle est justifié pour permettre aux utilisateurs de vérifier formellement des théorèmes mathématiques et l'exactitude de systèmes critiques. La bibliothèque standard de Coq dispose d'une axiomatisation des nombres réels et d'une bibliothèque de théorèmes d'analyse réelle. Malheureusement, cette bibliothèque souffre de nombreuses lacunes. Par exemple, les définitions des intégrales et des dérivées sont basées sur les types dépendants, ce qui les rend difficiles à utiliser dans la pratique. Cette thèse décrit d'abord l'état de l'art des différentes bibliothèques d'analyse réelle disponibles dans les assistants de preuve. Pour pallier les insuffisances de la bibliothèque standard de Coq, nous avons conçu une bibliothèque facile à utiliser : Coquelicot. Une façon plus facile d'écrire les formules et les théorèmes a été mise en place en utilisant des fonctions totales à la place des types dépendants pour écrire les limites, dérivées, intégrales et séries entières. Pour faciliter l'utilisation, la bibliothèque dispose d'un ensemble complet de théorèmes couvrant ces notions, mais aussi quelques extensions comme les intégrales à paramètres et les comportements asymptotiques. En plus, une hiérarchie algébrique permet d'appliquer certains théorèmes dans un cadre plus générique comme les nombres complexes pour les matrices. Coquelicot est une extension conservative de l'analyse classique de la bibliothèque standard de Coq et nous avons démontré les théorèmes de correspondance entre les deux formalisations. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur une épreuve du Baccalauréat, pour les définitions et les propriétés des fonctions de Bessel ainsi que pour la solution de l'équation des ondes en dimension 1.

Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, the definitions of integrals and derivatives are based on dependent types, which make them cumbersome to use in practice. This thesis first describes various state-of-the-art libraries available in proof assistants. To palliate the inadequacies of the Coq standard library, we have designed a user-friendly formalization of real analysis: Coquelicot. An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a…

Advisors/Committee Members: Boldo, Sylvie (thesis director), Melquiond, Guillaume (thesis director).

Subjects/Keywords: Preuve formelle; Assistant de preuve Coq; Analyse réelle; Analyse mathématique; Formal proof; Coq proof assistant; Real analysis; Mathematical analysis

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Lelay, C. (2015). Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis. (Doctoral Dissertation). Université Paris-Sud – Paris XI. Retrieved from http://www.theses.fr/2015PA112096

Chicago Manual of Style (16th Edition):

Lelay, Catherine. “Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis.” 2015. Doctoral Dissertation, Université Paris-Sud – Paris XI. Accessed January 21, 2021. http://www.theses.fr/2015PA112096.

MLA Handbook (7th Edition):

Lelay, Catherine. “Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis.” 2015. Web. 21 Jan 2021.

Vancouver:

Lelay C. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis. [Internet] [Doctoral dissertation]. Université Paris-Sud – Paris XI; 2015. [cited 2021 Jan 21]. Available from: http://www.theses.fr/2015PA112096.

Council of Science Editors:

Lelay C. Repenser la bibliothèque réelle de Coq : vers une formalisation de l'analyse classique mieux adaptée : Reinventing Coq's Reals library : toward a more suitable formalization of classical analysis. [Doctoral Dissertation]. Université Paris-Sud – Paris XI; 2015. Available from: http://www.theses.fr/2015PA112096


Université Paris-Sud – Paris XI

2. Nguyen, Thi Minh Tuyen. Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur.

Degree: Docteur es, Informatique, 2012, Université Paris-Sud – Paris XI

Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes. Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive.

On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification

Advisors/Committee Members: Marché, Claude (thesis director), Boldo, Sylvie (thesis director).

Subjects/Keywords: Arithmétique en virgule flottante; Programmes numériques; Analyse statique; Optimisations à la compilation; Plate-forme Why; Plate-forme Frama-C; Floating-point arithmetic; Numerical programs; Static analysis; Compile-time optimizations; The Why platform; The Frama-C platform

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Nguyen, T. M. T. (2012). Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur. (Doctoral Dissertation). Université Paris-Sud – Paris XI. Retrieved from http://www.theses.fr/2012PA112090

Chicago Manual of Style (16th Edition):

Nguyen, Thi Minh Tuyen. “Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur.” 2012. Doctoral Dissertation, Université Paris-Sud – Paris XI. Accessed January 21, 2021. http://www.theses.fr/2012PA112090.

MLA Handbook (7th Edition):

Nguyen, Thi Minh Tuyen. “Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur.” 2012. Web. 21 Jan 2021.

Vancouver:

Nguyen TMT. Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur. [Internet] [Doctoral dissertation]. Université Paris-Sud – Paris XI; 2012. [cited 2021 Jan 21]. Available from: http://www.theses.fr/2012PA112090.

Council of Science Editors:

Nguyen TMT. Taking architecture and compiler into account in formal proofs of numerical programs : Preuves formelles de programmes numériques en prenant en compte l'architecture et le compilateur. [Doctoral Dissertation]. Université Paris-Sud – Paris XI; 2012. Available from: http://www.theses.fr/2012PA112090

.