Systems and methods for model checking the precision of programs employing floating-point operations
US8539451B2 · kind B2 · utility
21Cited by
8References
19Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Apr 16, 2010 |
| Grant date | Sep 17, 2013 |
| Priority date | — |
| Expiry date | May 25, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Methods and systems for verifying the precision of a program that utilizes floating point operations are disclosed. Interval and affine arithmetic can be employed to build a model of the program including floating point operations and variables that are expressed as reals and integers, thereby permitting accurate determination of precision loss using a model checker. Abstract interpretation can be also employed to simplify the model. In addition, counterexample-guided abstraction refinement can be used to refine the values of parametric error constants introduced in the model.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.