[ list |
abstracts |
bib ]

## Certifying Solutions for Numerical Constraints

paper pdf
### Abstract

A large portion of software is used for numerical
computation in mathematics, physics and engineering. Among
the aspects that make verification in this domain difficult
is the need to quantify numerical errors, such as roundoff
errors and errors due to the use of approximate numerical
methods. Much of numerical software uses self-stabilizing
iterative algorithms, for example, to find solutions of
nonlinear equations. To support such algorithms, we present
a runtime verification technique that checks, given a
nonlinear equation and a tentative solution, whether this
value is indeed a solution to within a specified precision.
Our technique combines runtime verification approaches with
information about the analytical equation being solved. It
is independent of the algorithm used for finding the
solution and is therefore applicable to a wide range of
problems. We have implemented our technique for the Scala
programming language using our affine arithmetic library and
the macro facility of Scala 2.10.

### Citation

Eva Darulova and Viktor Kuncak.
Certifying solutions for numerical constraints.
In *Runtime Verification (RV)*, 2012.### BibTex Entry

@INPROCEEDINGS{DarulovaKuncak12CertifyingSolutionsNumericalConstraints,
author = {Eva Darulova and Viktor Kuncak},
title = {Certifying Solutions for Numerical Constraints},
booktitle = {Runtime Verification (RV)},
year = 2012,
localurl = {http://lara.epfl.ch/~kuncak/papers/DarulovaKuncak12CertifyingSolutionsNumericalConstraints.pdf}
}

[ list |
abstracts |
bib ]