FORWARD AND BACKWARD STATIC ANALYSIS FOR CRITICAL NUMERICAL ACCURACY IN FLOATING POINT PROGRAMS

Somasundaram Kanagasabapathi; MG Thushara

doi:10.7494/csci.2020.21.2.3421

Authors

Somasundaram Kanagasabapathi Department of Mathematics Amrita School of Engineering Amrita Vishwa Vidyapeetham Coimbatore-641112 Tamilnadu India.
MG Thushara Department of Computer Science Amrita Vishwa Vidyapeetham, Amritaputi, Keraka, India.

DOI:

https://doi.org/10.7494/csci.2020.21.2.3421

Keywords:

Abstract Interpretation, Backward Static Analysis, Floating-Point Numbers, Round-off Errors, Abstract domain

Abstract

In this article, we introduce a new static analysis for numerical accuracy. We
address the problem of determining the minimal accuracy on the inputs and on the intermediary results of a program containing foating-point computations in order to ensure a desired accuracy on the outputs. The main approach is to combine a forward and a backward static analysis, done by abstract interpretation. The backward analysis computes the minimal accuracy needed for the inputs and intermediary results of the program in order to ensure a desired accuracy on the results, specied by the user. In practice, the information collected by our analysis may help to optimize the formats used to represent the values stored in the variables of the program or to select the appropriate sensors. To illustrate our analysis, we have shown a prototype example with experimental results.

Downloads

Download data is not yet available.

References

Agency E.S.: European Space Agency, Ariane 501 Inquiry Board Report.

Tech. rep., , 1996. URL https://www:esa:int/For Media/Press Releases/

Ariane 501 - Presentation of Inquiry Board report.

Blanchet B., Cousot P., Cousot R., Feret J., Mauborgne L., Mine A., Monniaux D., Rival X.: A Static Analyzer for Large Safety-critical Software. In: SIGPLAN Not., vol. 38(5), pp. 196{207, 2003. ISSN 0362-1340. URL http://dx:doi:org/10:1145/780822:781153.

Chiang W.F., Baranowski M., Briggs I., Solovyev A., Gopalakrishnan G., Rakamari c Z.: Rigorous Floating-point Mixed-precision Tuning. In: SIGPLAN Not., vol. 52(1), pp. 300{315, 2017. ISSN 0362-1340. URL http://dx:doi:org/

:1145/3093333:3009846.

Cortesi A.: Widening Operators for Abstract Interpretation. In: 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pp. 31{40. 2008. ISSN 1551-0255. URL http://dx:doi:org/10:1109/SEFM:2008:20.

Cousot P.: Abstract interpretation: Achievements and perspectives. In: Proceedings of the SSGRR 2000 Computer and eBusiness International Conference, Compact Disk Paper 224 and Electronic Proceedings. Scuola Superiore G. Reiss Romoli, Italy, 2000.

Cousot P., Cousot R.: Abstract Interpretation: A Unied Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, pp. 238{252. ACM, New York, NY, USA, 1977. URL http://dx:doi:org/10:1145/512950:512973.

Cousot P., Cousot R.: Abstract interpretation and application to logic programs. In: The Journal of Logic Programming, vol. 13(2), pp. 103 { 179,

ISSN 0743-1066. URL http://dx:doi:org/https://doi:org/10:1016/

-1066(92)90030-7.

Cousot P., Cousot R.: A Galois Connection Calculus for Abstract Interpretation. In: SIGPLAN Not., vol. 49(1), pp. 3{4, 2014. ISSN 0362-1340. URL http: //dx:doi:org/10:1145/2578855:2537850.

Darulova E., Kuncak V.: Sound Compilation of Reals. In: SIGPLAN Not.,

vol. 49(1), pp. 235{248, 2014. ISSN 0362-1340. URL http://dx:doi:org/

:1145/2578855:2535874.

Delmas D., Goubault E., Putot S., Souyris J., Tekkal K., Vedrine F.: Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. In: M. Alpuente, B. Cook, C. Joubert, eds., Formal Methods for Industrial Critical Systems, pp. 53{69. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. ISBN 978-3-642-04570-7.

de Dinechin F., Lauter C., Melquiond G.: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. In: IEEE Transac-

tions on Computers, vol. 60(2), pp. 242{253, 2011. ISSN 0018-9340. URL

http://dx:doi:org/10:1109/TC:2010:128.

Gange G., Navas J.A., Schachte P., Sndergaard H., Stuckey P.J.: Abstract Interpretation over Non-lattice Abstract Domains. In: F. Logozzo, M. Fahndrich, eds., Static Analysis, pp. 6{24. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. ISBN 978-3-642-38856-9.

Goldberg D.: What Every Computer Scientist Should Know About Floatingpoint Arithmetic. In: ACM Comput. Surv., vol. 23(1), pp. 5{48, 1991. ISSN 0360-0300. URL http://dx:doi:org/10:1145/103162:103163.

Goubault E.: Static Analyses of the Precision of Floating-Point Operations. In: Proceedings of the 8th International Symposium on Static Analysis, SAS '01, pp. 234{259. Springer-Verlag, London, UK, UK, 2001. ISBN 3-540-42314-1. URL

http://dl:acm:org/citation:cfm?id=647170:718304.

Management I., Technology Division Washington D.: Patriot missile defense:Software problems led to system failure at Dhahran, Saudi Arabia. Tech. rep., Information Management and Technology Division, US General Accounting Ofce, 1992. URL ReportGAO/IMTEC-92-26.

Muller J.M.: On the denition of ulp(x). Tech. Rep. RR-5504, INRIA, 2005. URL https://hal:inria:fr/inria-00070503.

Revision I.: IEEE Standard for Floating-Point Arithmetic. In: IEEE Std 754-2008, pp. 1{70, 2008. URL http://dx:doi:org/10:1109/IEEESTD:2008:4610935.

Rubio-Gonzlez C., Nguyen C., Nguyen H.D., Demmel J., Kahan W., Sen K., Bailey D.H., Iancu C., Hough D.: Precimonious: Tuning assistant for

oatingpoint precision. In: SC '13: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis, pp. 1{12. 2013. ISSN 2167-4337.

URL http://dx:doi:org/10:1145/2503210:2503296.

Titolo L., Feliu M.A., Moscato M., Mu~noz C.A.: An Abstract Interpretation Framework for the Round-O Error Analysis of Floating-Point Programs. In: I. Dillig, J. Palsberg, eds., Verication, Model Checking, and Abstract Interpretation, Volume-10747, pp. 516{537. Springer International Publishing, Cham, 2018.

ISBN 978-3-319-73721-8.