User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

Sound Approximation of Programs with Elementary Functions


Darulova,  Eva
Group E. Darulova, Max Planck Institute for Software Systems, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Darulova, E., & Volkova, A. (2019). Sound Approximation of Programs with Elementary Functions. In I. Dillig, & S. Tasiran (Eds.), Computer Aided Verification (pp. 174-183). Berlin: Springer. doi:10.1007/978-3-030-25543-5_11.

Cite as: http://hdl.handle.net/21.11116/0000-0005-D520-6
Elementary function calls are a common feature in numerical programs. While their implementations in mathematical libraries are highly optimized, function evaluation is nonetheless very expensive compared to plain arithmetic. Full accuracy is, however, not always needed. Unlike arithmetic, where the performance difference between for example single and double precision floating-point arithmetic is relatively small, elementary function calls provide a much richer tradeoff space between accuracy and efficiency. Navigating this space is challenging, as guaranteeing the accuracy and choosing correct parameters for good performance of approximations is highly nontrivial. We present a fully automated approach and a tool which approximates elementary function calls inside small programs while guaranteeing overall user given error bounds. Our tool leverages existing techniques for roundoff error computation and approximation of individual elementary function calls and provides an automated methodology for the exploration of parameter space. Our experiments show that significant efficiency improvements are possible in exchange for reduced, but guaranteed, accuracy.