PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

Forward and backward static analysis for critical numerical accuracy in floating-point programs

Treść / Zawartość
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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.
Wydawca
Czasopismo
Rocznik
Tom
Strony
179--192
Opis fizyczny
Bibliogr. 19 poz., rys.
Twórcy
  • Amrita School of Engineering, Department of Computer Science and Applications, Amrita Vishwa Vidyapeetham, Amritapuri, India
  • Amrita School of Engineering, Department of Mathematics, Coimbatore, Amrita Vishwa Vidyapeetham, India
Bibliografia
  • [1] Ariane 501 Inquiry Board Report. Tech. rep., European Space Agency, 1996. https://www.esa.int/For Media/Press Releases/Ariane 501 - Presentation of I nquiry Board report.
  • [2] Blanchet B., Cousot P., Cousot R., Feret J., Mauborgne L., Min´e A., Monniaux D., Rival X.: A static analyzer for large safety-critical software, SIGPLAN Notices, vol. 38(5), pp. 196–207, 2003, https://doi.org/10.1145/780822.781153.
  • [3] Chiang W.F., Baranowski M., Briggs I., Solovyev A., Gopalakrishnan G., Rakamari´c Z.: Rigorous floating-point mixed-precision tuning, SIGPLAN Notices, vol. 52(1), pp. 300–315, 2017, https://doi.org/10.1145/3093333.3009846.
  • [4] Cortesi A.: Widening Operators for Abstract Interpretation. In: 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pp. 31–40, 2008. https://doi.org/10.1109/SEFM.2008.20.
  • [5] 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.
  • [6] Cousot P., Cousot R.: Abstract interpretation: a unified 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, 1977. https: //doi.org/10.1145/512950.512973.
  • [7] Cousot P., Cousot R.: Abstract interpretation and application to logic programs, The Journal of Logic Programming, vol. 13(2), pp. 103–179, 1992, https://doi.org/ 10.1016/0743-1066(92)90030-7.
  • [8] Cousot P., Cousot R.: A galois connection calculus for abstract interpretation, SIGPLAN Notices, vol. 49(1), pp. 3–4, 2014, https://doi.org/10.1145/2578855. 2537850.
  • [9] Darulova E., Kuncak V.: Sound compilation of reals, SIGPLAN Notices, vol. 49(1), pp. 235–248, 2014, https://doi.org/10.1145/2578855.2535874.
  • [10] Delmas D., Goubault E., Putot S., Souyris J., Tekkal K., V´edrine 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, 2009.
  • [11] Dinechin de F., Lauter C., Melquiond G.: Certifying the Floating-Point Implementation of an Elementary Function Using Gappa, IEEE Transactions on Computers, vol. 60(2), pp. 242–253, 2011, https://doi.org/10.1109/TC.2010.128.
  • [12] Gange G., Navas J.A., Schachte P., Søndergaard H., Stuckey P.J.: Abstract Interpretation over Non-lattice Abstract Domains. In: Logozzo F., F¨ahndrich M. (eds.), Static Analysis, pp. 6–24, Springer, Berlin, Heidelberg, 2013.
  • [13] Goldberg D.: What every computer scientist should know about floating-point arithmetic, ACM Computing Surveys, vol. 23(1), pp. 5–48, 1991. https://doi.org/ 10.1145/103162.103163.
  • [14] 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, 2001. http://dl.acm.org/citation.cfm?id= 647170.718304.
  • [15] IEEE Standard for Floating-Point Arithmetic. In: IEEE Std 754-2008, pp. 1–70, 2008. https://doi.org/10.1109/IEEESTD.2008.4610935.
  • [16] Muller J.M.: On the definition of ulp(x), Research Report, RR-5504, LIP RR-2005-09, INRIA, LIP, pp. 16, 2005. https://hal.inria.fr/inria-00070503.
  • [17] PATRIOT MISSILE DEFENSE. Software Problems Led to System Failure at Dhahran, Saudi Arabia, Report to the Chairman, Subcommittee on Investigations and Oversight, Committee on Science, Space, and Technology, House of Representatives, United States General Accounting Office, Information Management and Technology Division, 1992. http://www-users.math.umn.edu/∼arnold/ /disasters/GAO-IMTEC-92-96.pdf.
  • [18] Rubio-Gonz´alez C., Nguyen C., Nguyen H.D., Demmel J., Kahan W., Sen K., Bailey D.H., Iancu C., Hough D.: Precimonious: tuning assistant for floating- -point precision. In: SC ’13: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis, pp. 1–12, 2013. https://doi.org/10.1145/2503210.2503296.
  • [19] Titolo L., Feli´u M.A., Moscato M., Mu˜noz C.A.: An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In: I. Dillig, J. Palsberg (eds.), Verification, Model Checking, and Abstract Interpretation, vol. 10747, pp. 516–537, Springer International Publishing, Cham, 2018.
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-cff068f8-2df8-4fb7-bc46-fdb3fea9c177
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.