Lab for Automated Reasoning and Analysis LARA

SmartFloat: Numerical Error Estimator

SmartFloat is a numerical data type library for sound floating-point computations in Scala. The library can perform sound computations with ranges of floating-point numbers and estimate the roundoff errors commited.

For example:

def cubeRoot = {
  val a: AffineFloat = 10
  var xn = AffineFloat(1.6)
  for(i <- 1 until 5) {
      xn = xn * ((xn*xn*xn + 2.0*a)/(2.0*xn*xn*xn + a))
  }
  println(xn.toStringWithAbsErrors)
  println(xn.interval)
}  

will compute the cube root of 10 by Halley's method and provide an upper bound on the absolute floating-point roundoff error committed on the final result:

2.1544 (1.3346e-15)
[2.1544346900318816,2.154434690031885]

The source is now available on GitHub. The only dependency is a small native library that you need to compile for your own platform, but for Linux and Mac this works without issues.

There is also a poster and a presentation available.

Applications

The SmartFloat data type has also been used for certifying solutions of systems of nonlinear equations. The implementation uses Scala macros, which is an experimental feature coming in Scala 2.10. For this reason this code is to be regarded as experimental as well, but you are free to try it out.

Publications

E. Darulova, V. Kuncak. Trustworthy Numerical Computation in Scala. OOPSLA 2011. PDF

E. Darulova, V. Kuncak. Certifying Solutions for Numerical Constraints RV 2012. PDF

The SmartFloat library is maintained by Eva Darulova.

 
smartfloat.txt · Last modified: 2013/04/08 11:16 by evka