Institute of Electrical & Electronic Engineers
In this paper the authors provide a bound on the number of numeric operations (fixed or floating point) that can safely be performed before accuracy is lost. This work has important implications for control systems with safety-critical software, as these systems are now running fast enough and long enough for their errors to impact on their functionality. Furthermore, worst-case analysis would blindly advise the replacement of existing systems that have been successfully running for years. They present here a set of formal theorems validated by the PVS proof assistant. These theorems will allow code analyzing tools to produce formal certificates of accurate behavior.