TY - GEN
T1 - Static analysis of finite precision computations
AU - Goubault, Eric
AU - Putot, Sylvie
PY - 2011/2/1
Y1 - 2011/2/1
N2 - We define several abstract semantics for the static analysis of finite precision computations, that bound not only the ranges of values taken by numerical variables of a program, but also the difference with the result of the same sequence of operations in an idealized real number semantics. These domains point out with more or less detail (control point, block, function for instance) sources of numerical errors in the program and the way they were propagated by further computations, thus allowing to evaluate not only the rounding error, but also sensitivity to inputs or parameters of the program. We describe two classes of abstractions, a non relational one based on intervals, and a weakly relational one based on parametrized zonotopic abstract domains called affine sets, especially well suited for sensitivity analysis and test generation. These abstract domains are implemented in the Fluctuat static analyzer, and we finally present some experiments.
AB - We define several abstract semantics for the static analysis of finite precision computations, that bound not only the ranges of values taken by numerical variables of a program, but also the difference with the result of the same sequence of operations in an idealized real number semantics. These domains point out with more or less detail (control point, block, function for instance) sources of numerical errors in the program and the way they were propagated by further computations, thus allowing to evaluate not only the rounding error, but also sensitivity to inputs or parameters of the program. We describe two classes of abstractions, a non relational one based on intervals, and a weakly relational one based on parametrized zonotopic abstract domains called affine sets, especially well suited for sensitivity analysis and test generation. These abstract domains are implemented in the Fluctuat static analyzer, and we finally present some experiments.
UR - https://www.scopus.com/pages/publications/79251592546
U2 - 10.1007/978-3-642-18275-4_17
DO - 10.1007/978-3-642-18275-4_17
M3 - Conference contribution
AN - SCOPUS:79251592546
SN - 9783642182747
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 232
EP - 247
BT - Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings
T2 - 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
Y2 - 23 January 2011 through 25 January 2011
ER -