Imperial College London
Portrait Picture

ProfessorAlastairDonaldson

Faculty of Engineering, Department of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8266alastair.donaldson Website

 
 
//

Location

 

422Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Magron:2017:10.1145/3015465,
author = {Magron, V and Constantinides, G and Donaldson, AF},
doi = {10.1145/3015465},
journal = {ACM Transactions on Mathematical Software},
pages = {1--31},
title = {Certified roundoff error bounds using semidefinite programming},
url = {http://dx.doi.org/10.1145/3015465},
volume = {43},
year = {2017}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - 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 straightforward method such as interval arithmetic, sophisticated techniques are less straightforward to implement in a formal setting. Thus there is a need for methods that 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.
AU  - Magron,V
AU  - Constantinides,G
AU  - Donaldson,AF
DO  - 10.1145/3015465
EP  - 31
PY  - 2017///
SN  - 0098-3500
SP  - 1
TI  - Certified roundoff error bounds using semidefinite programming
T2  - ACM Transactions on Mathematical Software
UR  - http://dx.doi.org/10.1145/3015465
UR  - https://dl.acm.org/doi/10.1145/3015465
UR  - http://hdl.handle.net/10044/1/42670
VL  - 43
ER  -
Download