Intra-procedural optimization of the numerical accuracy of programs

Nasrine Damouche; Matthieu Martel; Alexandre Chapoutot

doi:10.1007/978-3-319-19458-5_3

Intra-procedural optimization of the numerical accuracy of programs

Nasrine Damouche
, Matthieu Martel
, Alexandre Chapoutot

University of Perpignan Via Domitia, DALI Team-Project
University of Montpellier (UMR MiVEGEC)

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.

langue originale	Anglais
titre	Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings
rédacteurs en chef	Matthias Güdemann, Manuel Núñez
Editeur	Springer Verlag
Pages	31-46
Nombre de pages	16
ISBN (Electronique)	9783319194578
Les DOIs	https://doi.org/10.1007/978-3-319-19458-5_3
état	Publié - 1 janv. 2015
Evénement	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norvcge Durée: 22 juin 2015 → 23 juin 2015

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9128
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Pays/Territoire	Norvcge
La ville	Oslo
période	22/06/15 → 23/06/15

Accès au document

10.1007/978-3-319-19458-5_3

Contient cette citation

Damouche, N., Martel, M., & Chapoutot, A. (2015). Intra-procedural optimization of the numerical accuracy of programs. Dans M. Güdemann, & M. Núñez (eds.), Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings (p. 31-46). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 9128). Springer Verlag. https://doi.org/10.1007/978-3-319-19458-5_3

Damouche, Nasrine ; Martel, Matthieu ; Chapoutot, Alexandre. / Intra-procedural optimization of the numerical accuracy of programs. Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings. Editeur / Matthias Güdemann ; Manuel Núñez. Springer Verlag, 2015. p. 31-46 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d0acf2e4513b470aa562676bf0e2c349,

title = "Intra-procedural optimization of the numerical accuracy of programs",

abstract = "Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.",

keywords = "Floating-point numbers, IEEE754 standard, Program transformation, Static analysis",

author = "Nasrine Damouche and Matthieu Martel and Alexandre Chapoutot",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2015.; 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 ; Conference date: 22-06-2015 Through 23-06-2015",

year = "2015",

month = jan,

day = "1",

doi = "10.1007/978-3-319-19458-5\_3",

language = "English",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "31--46",

editor = "Matthias G{\"u}demann and Manuel N{\'u}{\~n}ez",

booktitle = "Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings",

}

Damouche, N, Martel, M & Chapoutot, A 2015, Intra-procedural optimization of the numerical accuracy of programs. Dans M Güdemann & M Núñez (eds), Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 9128, Springer Verlag, p. 31-46, 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norvcge, 22/06/15. https://doi.org/10.1007/978-3-319-19458-5_3

Intra-procedural optimization of the numerical accuracy of programs. / Damouche, Nasrine; Martel, Matthieu; Chapoutot, Alexandre.
Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings. Ed. / Matthias Güdemann; Manuel Núñez. Springer Verlag, 2015. p. 31-46 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 9128).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Intra-procedural optimization of the numerical accuracy of programs

AU - Damouche, Nasrine

AU - Martel, Matthieu

AU - Chapoutot, Alexandre

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2015.

PY - 2015/1/1

Y1 - 2015/1/1

N2 - Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.

AB - Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.

KW - Floating-point numbers

KW - IEEE754 standard

KW - Program transformation

KW - Static analysis

U2 - 10.1007/978-3-319-19458-5_3

DO - 10.1007/978-3-319-19458-5_3

M3 - Conference contribution

AN - SCOPUS:84931083722

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 31

EP - 46

BT - Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings

A2 - Güdemann, Matthias

A2 - Núñez, Manuel

PB - Springer Verlag

T2 - 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015

Y2 - 22 June 2015 through 23 June 2015

ER -

Damouche N, Martel M, Chapoutot A. Intra-procedural optimization of the numerical accuracy of programs. Dans Güdemann M, Núñez M, rédacteurs en chef, Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings. Springer Verlag. 2015. p. 31-46. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-19458-5_3

Intra-procedural optimization of the numerical accuracy of programs

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation