Patent ID: 8539451
Filing Date: 2013-09-17
Classification: G06F

Abstract:
1. A method for verifying a program that utilizes floating point operations implemented by a processor employing a storage medium, the method comprising: modeling the variability in values of floating point variables and operations in the program by employing validation arithmetics to generate modeling variables, composed of at least one of reals and integers, for the floating point variables, wherein the modeling further comprises employing interval arithmetic to generate rounding functions for sub-normal numbers by introducing a sub-normal parametric error constant for at least one floating point operation precision type and for at least one sub-normal number range of the at least one floating point operation precision type, and wherein the sub-normal error constant is greater than or equal to the largest absolute error in the at least one sub-normal number range; generating a model for the program based on the modeling variables; performing model checking on the generated model to determine whether there are program instabilities due to loss of precision in floating point representation and operations in the program; and reporting error traces for any program instabilities found by the model checking.