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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings
Editors	Matthias Güdemann, Manuel Núñez
Publisher	Springer Verlag
Pages	31-46
Number of pages	16
ISBN (Electronic)	9783319194578
DOIs	https://doi.org/10.1007/978-3-319-19458-5_3
Publication status	Published - 1 Jan 2015
Event	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015 - Oslo, Norway Duration: 22 Jun 2015 → 23 Jun 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9128
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015
Country/Territory	Norway
City	Oslo
Period	22/06/15 → 23/06/15

Keywords

Floating-point numbers
IEEE754 standard
Program transformation
Static analysis

Access to Document

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

Cite this

Damouche, N., Martel, M., & Chapoutot, A. (2015). Intra-procedural optimization of the numerical accuracy of programs. In M. Güdemann, & M. Núñez (Eds.), Formal Methods for Industrial Critical Systems - 20th International Workshop, FMICS 2015, Proceedings (pp. 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. editor / Matthias Güdemann ; Manuel Núñez. Springer Verlag, 2015. pp. 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. in 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, pp. 31-46, 20th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2015, Oslo, Norway, 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In Güdemann M, Núñez M, editors, 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

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this