PRECiSA swMATH ID: 38041 Software Authors: Titolo, Laura; Feliú, Marco A.; Moscato, Mariano; Muñoz, César A. Description: An abstract interpretation framework for the round-off error analysis of floating-point programs. This paper presents an abstract interpretation framework for the round-off error analysis of floating-point programs. This framework defines a parametric abstract analysis that computes, for each combination of ideal and floating-point execution path of the program, a sound over-approximation of the accumulated floating-point round-off error that may occur. In addition, a Boolean expression that characterizes the input values leading to the computed error approximation is also computed. An abstraction on the control flow of the program is proposed to mitigate the explosion of the number of elements generated by the analysis. Additionally, a widening operator is defined to ensure the convergence of recursive functions and loops. An instantiation of this framework is implemented in the prototype tool PRECiSA that generates formal proof certificates stating the correctness of the computed round-off errors. Homepage: https://link.springer.com/chapter/10.1007%2F978-3-319-73721-8_24 Related Software: RangeLab; z3; ASTREE; Frama-C; PVS; Reluplex; AI2; PyTorch; Gurobi; Coq; Daisy; GitHub; FPTuner; dReal; mctoolbox; cvc3; Gappa; ACSL; HOL Light Cited in: 4 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year An abstract interpretation framework for the round-off error analysis of floating-point programs. Zbl 1446.68036Titolo, Laura; Feliú, Marco A.; Moscato, Mariano; Muñoz, César A. 2018 all top 5 Cited by 11 Authors 2 Moscato, Mariano M. 2 Muñoz, César A. 2 Titolo, Laura 1 Bobot, François 1 Dahlqvist, Fredrik 1 Dutle, Aaron 1 Feliú, Marco A. 1 Jia, Kai 1 Rakamarić, Zvonimir 1 Rinard, Martin C. 1 Salvia, Rocco Cited in 1 Serial 1 Formal Aspects of Computing Cited in 2 Fields 4 Numerical analysis (65-XX) 3 Computer science (68-XX) Citations by Year