Certified Roundoff Error Bounds Using Semidefinite Programming.

File Description SizeFormat 
1507.03331v1.pdfPublished version881.49 kBAdobe PDFView/Open
Title: Certified Roundoff Error Bounds Using Semidefinite Programming.
Authors: Magron, V
Constantinides, GA
Donaldson, AF
Item Type: Working Paper
Abstract: Roundoff errors cannot be avoided when implementing numerical programs with finite precision. The ability to reason about rounding is especially important if one wants to explore a range of potential representations, for instance for FPGAs or custom hardware implementation. This problem becomes challenging when the program does not employ solely linear operations as non-linearities are inherent to many interesting computational problems in real-world applications. Existing solutions to reasoning are limited in the presence of nonlinear correlations between variables, leading to either imprecise bounds or high analysis time. Furthermore, while it is easy to implement a straightforward method such as interval arithmetic, sophisticated techniques are less straightforward to implement in a formal setting. Thus there is a need for methods which output certificates that can be formally validated inside a proof assistant. We present a framework to provide upper bounds on absolute roundoff errors. This framework is based on optimization techniques employing semidefinite programming and sums of squares certificates, which can be formally checked inside the Coq theorem prover. Our tool covers a wide range of nonlinear programs, including polynomials and transcendental operations as well as conditional statements. We illustrate the efficiency and precision of this tool on non-trivial programs coming from biology, optimization and space control. Our tool produces more precise error bounds for 37 percent of all programs and yields better performance in 73 percent of all programs.
Issue Date: 13-Jul-2015
URI: http://hdl.handle.net/10044/1/29366
Copyright Statement: © 2015 The Authors
Sponsor/Funder: Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Royal Academy Of Engineering
Imagination Technologies Ltd
Funder's Grant Number: EP/I012036/1
EP/I020357/1
11908 (EP/K034448/1)
Prof Constantinides Chair
Prof Constantinides Chair
Keywords: cs.NA
hardware precision tuning
roundoff error
numerical accuracy
floating-point arithmetic
fixed-precision arithmetic
semidefinite programming
sums of squares
correlation sparsity pattern
proof assistant
formal verification
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx