Taking architecture and compiler into account in formal proofs of numerical programs
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 thesi...
Main Author: | |
---|---|
Language: | English |
Published: |
Université Paris Sud - Paris XI
2012
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-00710193 http://tel.archives-ouvertes.fr/docs/00/71/01/93/PDF/VD2_NGUYEN_Thi-Minh-Tuyen_11062012.pdf |
id |
ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-00710193 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-CCSD-oai-tel.archives-ouvertes.fr-tel-007101932014-10-08T03:28:31Z http://tel.archives-ouvertes.fr/tel-00710193 2012PA112090 http://tel.archives-ouvertes.fr/docs/00/71/01/93/PDF/VD2_NGUYEN_Thi-Minh-Tuyen_11062012.pdf Taking architecture and compiler into account in formal proofs of numerical programs Nguyen, Thi Minh Tuyen [INFO:INFO_OH] Computer Science/Other [INFO:INFO_OH] Informatique/Autre Floating-point arithmetic Numerical programs Static analysis Compile-time optimizations The Why platform The Frama-C platform 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 2012-06-11 eng PhD thesis Université Paris Sud - Paris XI |
collection |
NDLTD |
language |
English |
sources |
NDLTD |
topic |
[INFO:INFO_OH] Computer Science/Other [INFO:INFO_OH] Informatique/Autre Floating-point arithmetic Numerical programs Static analysis Compile-time optimizations The Why platform The Frama-C platform |
spellingShingle |
[INFO:INFO_OH] Computer Science/Other [INFO:INFO_OH] Informatique/Autre Floating-point arithmetic Numerical programs Static analysis Compile-time optimizations The Why platform The Frama-C platform Nguyen, Thi Minh Tuyen Taking architecture and compiler into account in formal proofs of numerical programs |
description |
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 |
author |
Nguyen, Thi Minh Tuyen |
author_facet |
Nguyen, Thi Minh Tuyen |
author_sort |
Nguyen, Thi Minh Tuyen |
title |
Taking architecture and compiler into account in formal proofs of numerical programs |
title_short |
Taking architecture and compiler into account in formal proofs of numerical programs |
title_full |
Taking architecture and compiler into account in formal proofs of numerical programs |
title_fullStr |
Taking architecture and compiler into account in formal proofs of numerical programs |
title_full_unstemmed |
Taking architecture and compiler into account in formal proofs of numerical programs |
title_sort |
taking architecture and compiler into account in formal proofs of numerical programs |
publisher |
Université Paris Sud - Paris XI |
publishDate |
2012 |
url |
http://tel.archives-ouvertes.fr/tel-00710193 http://tel.archives-ouvertes.fr/docs/00/71/01/93/PDF/VD2_NGUYEN_Thi-Minh-Tuyen_11062012.pdf |
work_keys_str_mv |
AT nguyenthiminhtuyen takingarchitectureandcompilerintoaccountinformalproofsofnumericalprograms |
_version_ |
1716716155405598720 |