Programming with Numerical Uncertainties

Created by W.Langdon from gp-bibliography.bib Revision:1.4202

  author =       "Eva Darulova",
  title =        "Programming with Numerical Uncertainties",
  school =       "EPFL",
  year =         "2014",
  address =      "Lausanne, Switzerland",
  keywords =     "genetic algorithms, genetic programming, ECJ,
                 floating-point arithmetic, fixed-point arithmetic,
                 roundoff errors, numerical accuracy, static analysis,
                 runtime verification, software synthesis",
  URL =          "",
  URL =          "",
  URL =          "",
  size =         "172 pages",
  abstract =     "Numerical software, common in scientific computing or
                 embedded systems, inevitably uses an approximation of
                 the real arithmetic in which most algorithms are
                 designed. In many domains, roundoff errors are not the
                 only source of inaccuracy and measurement as well as
                 truncation errors further increase the uncertainty of
                 the computed results. Adequate tools are needed to help
                 users select suitable approximations (data types and
                 algorithms) which satisfy their accuracy requirements,
                 especially for safety-critical applications.
                 Determining that a computation produces accurate
                 results is challenging. Roundoff errors and error
                 propagation depend on the ranges of variables in
                 complex and non-obvious ways; even determining these
                 ranges accurately for nonlinear programs poses a
                 significant challenge. In numerical loops, roundoff
                 errors grow, in general, unboundedly. Finally, due to
                 numerical errors, the control flow in the
                 finite-precision implementation may diverge from the
                 ideal real-valued one by taking a different branch and
                 produce a result that is far-off of the expected one.
                 In this thesis, we present techniques and tools for
                 automated and sound analysis, verification and
                 synthesis of numerical programs. We focus on numerical
                 errors due to roundoff from floating-point and
                 fixed-point arithmetic, external input uncertainties or
                 truncation errors. Our work uses interval or affine
                 arithmetic together with Satisfiability Modulo Theories
                 (SMT) technology as well as analytical properties of
                 the underlying mathematical problems. This combination
                 of techniques enables us to compute sound and yet
                 accurate error bounds for nonlinear computations,
                 determine closed-form symbolic invariants for unbounded
                 loops and quantify the effects of discontinuities on
                 numerical errors. We can furthermore certify the
                 results of self-correcting iterative algorithms.
                 Accuracy usually comes at the expense of resource
                 efficiency: more precise data types need more time,
                 space and energy. We propose a programming model where
                 the scientist writes his or her numerical program in a
                 real-valued specification language with explicit error
                 annotations. It is then the task of our verifying
                 compiler to select a suitable floating-point or
                 fixed-point data type which guarantees the needed
                 accuracy. Sometimes accuracy can be gained by simply
                 re-arranging the non-associative finite-precision
                 computation. We present a scalable technique that
                 searches for a more optimal evaluation order and show
                 that the gains can be substantial. We have implemented
                 all our techniques and evaluated them on a number of
                 benchmarks from scientific computing and embedded
                 systems, with promising results.",
  notes =        "'Synthesizing Accurate Fixed-Point

                 'Difficulty of Simple Encoding into SMT

                 Supervisor Viktor Kuncak Thesis number 6343 (2014)",

Genetic Programming entries for Eva Darulova