CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Gabriele Paganelli (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013; Timisoara; Romania; 23 September 2013 through 26 September 2013 p. 209-216. (2014)
[Konferensbidrag, refereegranskat]

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.


Article number 6821152



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2013-12-21. Senast ändrad 2015-10-26.
CPL Pubid: 190347

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)