Certified roundoff error bounds using semidefinite programming

File Description SizeFormat 
Victor_TOMS16.pdfAccepted version804.16 kBAdobe PDFDownload
Title: Certified roundoff error bounds using semidefinite programming
Author(s): Magron, V
Constantinides, GA
Donaldson, A
Item Type: Journal Article
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 implementations. 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 possibly lead to either inaccurate bounds or high analysis time in the presence of nonlinear correlations between variables. Furthermore, while it is easy to implement a straight- forward 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 of floating-point nonlinear programs. This framework is based on optimization techniques employing semidefinite programming and sums of squares certificates, which can be checked inside the Coq theorem prover to provide formal roundoff error bounds for polynomial programs. 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 accurate error bounds for 23 % of all programs and yields better performance in 66 % of all programs.
Publication Date: 23-Mar-2018
Date of Acceptance: 6-Nov-2016
URI: http://hdl.handle.net/10044/1/42670
DOI: https://dx.doi.org/10.1145/3015465
ISSN: 1557-7295
Publisher: Association for Computing Machinery (ACM)
Journal / Book Title: ACM Transactions on Mathematical Software
Volume: 43
Issue: 4
Sponsor/Funder: Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Royal Academy Of Engineering
Imagination Technologies Ltd
Funder's Grant Number: EP/I020357/1
11908 (EP/K034448/1)
Prof Constantinides Chair
Prof Constantinides Chair
Copyright Statement: © 2016 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Mathematical Software (TOMS), Vol. 43, Iss. 4, (March 2016) https://dl.acm.org/citation.cfm?doid=3034774.3015465
Keywords: 0802 Computation Theory And Mathematics
0806 Information Systems
Numerical & Computational Mathematics
Publication Status: Published
Article Number: ARTN 34
Open Access location: https://arxiv.org/abs/1507.03331
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering

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

Creative Commons