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:

You searched for subject:(Optimisations la compilation). One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


Université Paris-Sud – Paris XI

1. 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 26, 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. 26 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 26]. 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

.