### Abstract

it is normal to “limit our study to the semantics

dealing with numerical precision” (Martel, 2005). On the other

hand, there is a great deal of work on the reliability of

programs that essentially ignores the numerics. The thesis

of this paper is that there is a class of problems that fall

between these two, which could be described as “does the lowlevel

arithmetic implement the high-level mathematics”. Many

of these problems arise because mathematics, particularly

the mathematics of the complex numbers, is more difficult

than expected: for example the complex function log is not

continuous, writing down a program to compute an inverse

function is more complicated than just solving an equation,

and many algebraic simplification rules are not universally

valid.

The good news is that these problems are theoretically

capable of being solved, and are practically close to being solved,

but not yet solved, in several real-world examples. However,

there is still a long way to go

Language | English |
---|---|

Title of host publication | Proceedings of SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing |

Place of Publication | Piscataway |

Publisher | IEEE |

Pages | 83-88 |

Number of pages | 6 |

ISBN (Print) | 9781467350266 |

DOIs | |

Status | Published - 2012 |

Event | SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing - Timisoara, Romania Duration: 25 Sep 2012 → 28 Sep 2012 |

### Conference

Conference | SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing |
---|---|

Country | Romania |

City | Timisoara |

Period | 25/09/12 → 28/09/12 |

### Fingerprint

### Cite this

*Proceedings of SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing*(pp. 83-88). Piscataway: IEEE. https://doi.org/10.1109/SYNASC.2012.68

**Program Verification in the presence of complex numbers, functions with branch cuts etc.** / Davenport, James; Bradford, Russell; England, Matthew; Wilson, David.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*Proceedings of SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing.*IEEE, Piscataway, pp. 83-88, SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, 25/09/12. https://doi.org/10.1109/SYNASC.2012.68

}

TY - GEN

T1 - Program Verification in the presence of complex numbers, functions with branch cuts etc

AU - Davenport, James

AU - Bradford, Russell

AU - England, Matthew

AU - Wilson, David

PY - 2012

Y1 - 2012

N2 - In considering the reliability of numerical programs,it is normal to “limit our study to the semanticsdealing with numerical precision” (Martel, 2005). On the otherhand, there is a great deal of work on the reliability ofprograms that essentially ignores the numerics. The thesisof this paper is that there is a class of problems that fallbetween these two, which could be described as “does the lowlevelarithmetic implement the high-level mathematics”. Manyof these problems arise because mathematics, particularlythe mathematics of the complex numbers, is more difficultthan expected: for example the complex function log is notcontinuous, writing down a program to compute an inversefunction is more complicated than just solving an equation,and many algebraic simplification rules are not universallyvalid.The good news is that these problems are theoreticallycapable of being solved, and are practically close to being solved,but not yet solved, in several real-world examples. However,there is still a long way to go

AB - In considering the reliability of numerical programs,it is normal to “limit our study to the semanticsdealing with numerical precision” (Martel, 2005). On the otherhand, there is a great deal of work on the reliability ofprograms that essentially ignores the numerics. The thesisof this paper is that there is a class of problems that fallbetween these two, which could be described as “does the lowlevelarithmetic implement the high-level mathematics”. Manyof these problems arise because mathematics, particularlythe mathematics of the complex numbers, is more difficultthan expected: for example the complex function log is notcontinuous, writing down a program to compute an inversefunction is more complicated than just solving an equation,and many algebraic simplification rules are not universallyvalid.The good news is that these problems are theoreticallycapable of being solved, and are practically close to being solved,but not yet solved, in several real-world examples. However,there is still a long way to go

UR - http://synasc12.info.uvt.ro/

UR - http://dx.doi.org/10.1109/SYNASC.2012.68

U2 - 10.1109/SYNASC.2012.68

DO - 10.1109/SYNASC.2012.68

M3 - Conference contribution

SN - 9781467350266

SP - 83

EP - 88

BT - Proceedings of SYNASC 2012: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing

PB - IEEE

CY - Piscataway

ER -