@inproceedings{dar-kun-maj-sah-13-aa-polev,
  author = {Darulov{\'a}, Eva and Kuncak, Viktor and Majumdar, Rupak and Saha, Indranil},
  title = {Synthesis of Fixed-Point Programs},
  booktitle = {Proceedings of the International Conference on Embedded Software (EMSOFT)},
  year = 2013,
  month = sep,
  location = {Montreal, CA},
  doi = {10.1109/EMSOFT.2013.6658600},
  pages = {1-10},
  comment = {Rearranges computation of a polynomial so as to minimize the error when evaluated with fixed point operations. Shows that the problem is NP-hard. Uses genetic algorithm to experiment with the formulas, and AA to evaluate the accuracy of each formula.},
  abstract = {Several problems in the implementations of control systems, signal-processing systems, and scientific computing systems reduce to compiling a polynomial expression over the reals into an imperative program using fixed-point arithmetic. Fixed-point arithmetic only approximates real values, and its operators do not have the fundamental properties of real arithmetic, such as associativity. Consequently, a naive compilation process can yield a program that significantly deviates from the real polynomial, whereas a different order of evaluation can result in a program that is close to the real value on all inputs in its domain. We present a compilation scheme for real-valued arithmetic expressions to fixed-point arithmetic programs. Given a real-valued polynomial expression t, we find an expression t' that is equivalent to t over the reals, but whose implementation as a series of fixed-point operations minimizes the error between the fixed-point value and the value of t over the space of all inputs. We show that the corresponding decision problem, checking whether there is an implementation t' of t whose error is less than a given constant, is NP-hard. We then propose a solution technique based on genetic programming. Our technique evaluates the fitness of each candidate program using a static analysis based on affine arithmetic. We show that our tool can significantly reduce the error in the fixed-point implementation on a set of linear control system benchmarks. For example, our tool found implementations whose errors are only one half of the errors in the original fixed-point expressions.}
}