Xấp xỉ chính xác của số học dấu phẩy động IEEE 754 cho kiểm tra chương trình

Aharoni, M., Asaf, S., Fournier, L., Koyfman, A., & Nagel, R. (2003). FPGen — a test generation framework for datapath floating-point verification. In Eighth IEEE international high-level design validation and test workshop. https://doi.org/10.1109/HLDVT.2003.1252469 (pp. 17–22). San Francisco: IEEE Computer Society. Aho, A.V., Lam, M.S., Sethi, R., & Ullman, J.D. (2006). Compilers: principles, techniques, and tools, 2nd edn. Boston: Addison-Wesley Longman Publishing Co., Inc. Arm Limited: Arm® Architecture Reference Manual, Armv8, for A-profile architecture edn. (2021). https://developer.arm.com/architectures/cpu-architecture/a-profile/docs. Last accessed on October 27th, 2021. Bagnara, R., Carlier, M., Gori, R., & Gotlieb, A. (2013). Symbolic path-oriented test data generation for floating-point programs. In Proceedings of the 6th IEEE international conference on software testing, verification and validation. https://doi.org/10.1109/ICST.2013.17. Luxembourg City: IEEE Press. Bagnara, R., Carlier, M., Gori, R., & Gotlieb, A. (2016). Exploiting binary floating-point representations for constraint propagation. INFORMS Journal on Computing, 28(1), 31–46. https://doi.org/10.1287/ijoc.2015.0663. Bagnara, R., Chiari, M., Gori, R., & Bagnara, A. (2021). A practical approach to verification of floating-point C/C++ programs with math.h/cmath functions. ACM Transactions on Software Engineering and Methodology, 30(1), 9:1–9:53. https://doi.org/10.1145/3410875. Barr, E.T., Vo, T., Le, V., & Su, Z. (2013). Automatic detection of floating-point exceptions. In The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’13, Rome, Italy - January 23 - 25, 2013. https://doi.org/10.1145/2429069.2429133 (pp. 549–560). Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., & Tinelli, C. (2011). CVC4. In Computer aided verification, proceedings of the 23rd international conference (CAV 2011), Lecture notes in computer science. https://doi.org/10.1007/978-3-642-22110-1_14, (Vol. 6806 pp. 171–177). Snowbird: Springer. Barrett, C.W., & Tinelli, C. (2018). Satisfiability modulo theories. In E.M. Clarke, T.A. Henzinger, H. Veith, & R. Bloem (Eds.) Handbook of model checking. https://doi.org/10.1007/978-3-319-10575-8_11 (pp. 305–343). Springer. Botella, B., Gotlieb, A., & Michel, C. (2006). Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16(2), 97–121. https://doi.org/10.1002/stvr.333. Brain, M., D’Silva, V., Griggio, A., Haller, L., & Kroening, D. (2014). Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design, 45(2), 213–245. https://doi.org/10.1007/s10703-013-0203-7. Brain, M., Schanda, F., & Sun, Y. (2019). Building better bit-blasting for floating-point problems. In Tools and algorithms for the construction and analysis of systems, proceedings of the 25th international conference (TACAS 2019), Part I, lecture notes in computer science. https://doi.org/10.1007/978-3-030-17462-0_5, (Vol. 11427 pp. 79–98). Springer. Brain, M., Tinelli, C., & Rümmer, P. (2015). T-wahl: An automatable formal semantics for IEEE-754 floating-point arithmetic. In 22nd IEEE symposium on computer arithmetic (ARITH 2015). https://doi.org/10.1109/ARITH.2015.26 (pp. 160–167). Lyon: IEEE. Cimatti, A., Griggio, A., Schaafsma, B.J., & Sebastiani, R. (2013). The mathSAT5 SMT solver. In Tools and algorithms for the construction and analysis of systems, proceedings of the 19th international conference (TACAS 2013), lecture notes in computer science. https://doi.org/10.1007/978-3-642-36742-7_7, (Vol. 7795 pp. 93–107). Springer. Clarke, L.A., & Richardson, D.J. (1985). Applications of symbolic evaluation. Journal of Systems and Software, 5(1), 15–35. https://doi.org/10.1016/0164-1212(85)90004-4. Cousot, P., & Cousot, R. (1977). Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the fourth annual ACM symposium on principles of programming languages. https://doi.org/10.1145/512950.512973 (pp. 238–252). Los Angeles: ACM Press. Cuyt, A., Kuterna, P., Verdonk, B., & Verschaeren, D. (2002). Underflow revisited. CALCOLO, 39(3), 169–179. https://doi.org/10.1007/s100920200003. de Moura, L.M., & Bjørner, N. (2008). Z3: an efficient SMT solver. In Tools and algorithms for the construction and analysis of systems, proceedings of the 14th international conference (TACAS 2008), lecture notes in computer science. https://doi.org/10.1007/978-3-540-78800-3_24, (Vol. 4963 pp. 337–340). Springer. Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., & Védrine, F. (2009). Towards an industrial use of FLUCTUAT on safety-critical avionics software. In Formal methods for industrial critical systems, proceedings of the 14th international workshop (FMICS 2009), lecture notes in computer science. https://doi.org/10.1007/978-3-642-04570-7_6, (Vol. 5825 pp. 53–69). Eindhoven: Springer. Fiedler, G. (2021). Floating point determinism. Gaffer on games blog, February 24, 2019. https://gafferongames.com/post/floating_point_determinism/ (2010) Last accessed on October 28th. Gallois-Wong, D., Boldo, S., & Cuoq, P. (2020). Optimal inverse projection of floating-point addition. Numerical Algorithms, 83(3), 957–986. https://doi.org/10.1007/s11075-019-00711-z. Gotlieb, A., Botella, B., & Rueher, M. (1998). Automatic test data generation using constraint solving techniques. In Proceedings of the 1998 ACM SIGSOFT international symposium on software testing and analysis, ISSTA ’98. https://doi.org/10.1145/271771.271790 (pp. 53–62). New York: ACM. Gotlieb, A., Botella, B., & Rueher, M. (2000). A CLP framework for computing structural test data. In Computational logic — CL 2000: first international conference london, UK, July 24–28, 2000 Proceedings. https://doi.org/10.1007/3-540-44957-4_27(pp. 399–413). Springer. The Institute of Electrical and Electronics Engineers, Inc.: IEEE Standard for Floating-Point Arithmetic, IEEE Std 754-2008 (revision of IEEE Std 754-1985) edn. (2008). Available at http://ieeexplore.ieee.org/servlet/opac?punumber=4610933. Intel Corporation. Intel® 64 and IA-32 Architectures Software Developer Manuals, 325462-075us edn. (2021). https://www.intel.com/content/www/us/en/developer/articles/technical/intel-sdm.html. Last accessed on October 27th, 2021. King, J.C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385–394. https://doi.org/10.1145/360248.360252. Kornerup, P., Lefevre, V., Louvet, N., & Muller, J.M. (2009). On the computation of correctly-rounded sums. In Proceedings of the 19th IEEE symposium on computer arithmetic (ARITH 2009). https://doi.org/10.1109/ARITH.2009.16 (pp. 155–160). Portland. Marre, B., Bobot, F., & Chihani, Z. (2017). Real behavior of floating point numbers. In Proceedings of the 15th international workshop on satisfiability modulo theories, CEUR workshop proceedings, (Vol. 1889 pp. 50–62). Marre, B., & Michel, C. (2010). Improving the floating point addition and subtraction constraints. In D. Cohen (Ed.) Proceedings of the 16th international conference on principles and practice of constraint programming (CP 2010), lecture notes in computer science. https://doi.org/10.1007/978-3-642-15396-9_30, (Vol. 6308 pp. 360–367). St. Andrews: Springer. Michel, C. (2002). Exact projection functions for floating point number constraints. In Proceedings of the 7th international symposium on artificial intelligence and mathematics. Fort Lauderdale. Michel, C., Rueher, M., & Lebbah, Y. (2001). Solving constraints over floating-point numbers. In Principles and practice of constraint programming - CP 2001, 7th international conference, CP 2001, paphos, cyprus, november 26 - december 1, 2001, proceedings. https://doi.org/10.1007/3-540-45578-7_36 (pp. 524–538). Miné, A. (2004). Relational abstract domains for the detection of floating-point run-time errors. In Programming languages and systems, proceedings of the 13th european symposium on programming (ESOP 2004), lecture notes in computer science. https://doi.org/10.1007/978-3-540-24725-8_2, (Vol. 2986 pp. 3–17). Barcelona: Springer. Monniaux, D. (2008). The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems, 30(3), 12:1–12:41. https://doi.org/10.1145/1353445.1353446. Müller, S.M., & Paul, W.J. (2000). Computer architecture - complexity and correctness springer. https://doi.org/10.1007/978-3-662-04267-0. Rump, S.M. (2013). Accurate solution of dense linear systems, Part II: Algorithms using directed rounding. Journal of Computational and Applied Mathematics, 242, 185–212. https://doi.org/10.1016/j.cam.2012.09.024. Rump, S.M., & Ogita, T. (2007). Super-fast validated solution of linear systems. Journal of Computational and Applied Mathematics, 199(2), 199–206. Special Issue on Scientific Computing, Computer Arithmetic, and Validated Numerics (SCAN 2004). Watte, J. (2021). Floating point determinism. Gamedev.net Forum, June 30, 2008. https://www.gamedev.net/forums/topic/499435-floating-point-determinism/ (2008) Last accessed on October 28th. Wu, X., Li, L., & Zhang, J. (2017). Symbolic execution with value-range analysis for floating-point exception detection. In 24th asia-pacific software engineering conference, APSEC 2017, Nanjing, China, December 4–8, 2017. https://doi.org/10.1109/APSEC.2017.6 (pp. 1–10).