A Mixed Real and Floating-Point Solver


Rocco Salvia, Laura Titolo, Marco A. Feliu, Mariano M. Moscato, Cesar A. Munoz, Zvonimir Rakamaric. 11th NASA Formal Methods Symposium (NFM 2019), Houston, TX, USA.
[pdf] [bib]

Abstract: Reasoning about mixed real and floating-point constraints is essential for developing accurate analysis tools for floating-point programs. This paper presents FPRoCK, a prototype tool for solving mixed real and floating-point formulas. FPRoCK transforms a mixed formula into an equisatisfiable one over the reals. This formula is then solved using an off-the-shelf SMT solver. FPRoCK is also integrated with the PRECiSA static analyzer, which computes a sound estimation of the round-off error of a floating-point program. It is used to detect infeasible computational paths, thereby improving the accuracy of PRECiSA.


  author = {Rocco Salvia and Laura Titolo and Marco A. Feli\'{u} and
Mariano M. Moscato and C\'{e}sar A. Mu\~{n}oz and Zvonimir Rakamari\'c}, title = {A Mixed Real and Floating-Point Solver}, booktitle = {Proceedings of the 11th NASA Formal Methods Symposium (NFM)},
year = {2019},
note = {to appear}