### Skapa referens, olika format (klipp och klistra)

**Harvard**

Paganelli, G. och Ahrendt, W. (2014) *Verifying (in-)stability in floating-point programs by increasing precision using SMT solvers*.

** BibTeX **

@conference{

Paganelli2014,

author={Paganelli, Gabriele and Ahrendt, Wolfgang},

title={Verifying (in-)stability in floating-point programs by increasing precision using SMT solvers},

booktitle={15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013; Timisoara; Romania; 23 September 2013 through 26 September 2013},

isbn={978-147993035-7},

pages={209-216},

abstract={When computing with floating-point numbers, programmers choose a certain floating-point precision (like, for instance, float or double) upfront, for each variable. However, whether the chosen precision is appropriate for the computation at hand, and vice versa, is difficult to judge. One way is to increase the precision, and observe whether the result of the computation changes too much, in which case the computation with the original precisions is considered 'unstable'. This effect may be exhibited with certain inputs, and not with others. With a classical testing approach, inputs that show instability can be very difficult to find. Moreover, testing can only show instability, not stability. In this paper, we present an approach, and its implementation, which can formally prove that an increased precision causes only a limited (quantified) change of the result. Alternatively, if the computation is not stable, the method returns inputs that exhibit this. We use methods from program verification, connecting to a novel SMT (satisfiability modulo theories) solver for floating-point number constraints. The user augments the program P with assertions on the expected stability bound. The system then creates a new program P', a certain kind of merge of P with a higher precision copy of P, computes the weakest precondition of P' w.r.t. these assertions, and feeds the resulting formula to the SMT solver, which then proves stability or alternatively returns data for a test exhibiting unstability, to be used for further analysis. The implementation of the system targets a toy language but supports the IEEE standard in a realistic manner. The paper describes the method and its implementation, reports experiments, and discusses the results.},

year={2014},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 190347

A1 Paganelli, Gabriele

A1 Ahrendt, Wolfgang

T1 Verifying (in-)stability in floating-point programs by increasing precision using SMT solvers

YR 2014

T2 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013; Timisoara; Romania; 23 September 2013 through 26 September 2013

SN 978-147993035-7

SP 209

OP 216

AB When computing with floating-point numbers, programmers choose a certain floating-point precision (like, for instance, float or double) upfront, for each variable. However, whether the chosen precision is appropriate for the computation at hand, and vice versa, is difficult to judge. One way is to increase the precision, and observe whether the result of the computation changes too much, in which case the computation with the original precisions is considered 'unstable'. This effect may be exhibited with certain inputs, and not with others. With a classical testing approach, inputs that show instability can be very difficult to find. Moreover, testing can only show instability, not stability. In this paper, we present an approach, and its implementation, which can formally prove that an increased precision causes only a limited (quantified) change of the result. Alternatively, if the computation is not stable, the method returns inputs that exhibit this. We use methods from program verification, connecting to a novel SMT (satisfiability modulo theories) solver for floating-point number constraints. The user augments the program P with assertions on the expected stability bound. The system then creates a new program P', a certain kind of merge of P with a higher precision copy of P, computes the weakest precondition of P' w.r.t. these assertions, and feeds the resulting formula to the SMT solver, which then proves stability or alternatively returns data for a test exhibiting unstability, to be used for further analysis. The implementation of the system targets a toy language but supports the IEEE standard in a realistic manner. The paper describes the method and its implementation, reports experiments, and discusses the results.

LA eng

DO 10.1109/SYNASC.2013.35

LK http://dx.doi.org/10.1109/SYNASC.2013.35

OL 30