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.

Citation

Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric
A Mixed Real and Floating-Point Solver
Proceedings of the 11th NASA Formal Methods Symposium (NFM), 11460: 363--370, doi:10.1007/978-3-030-20652-9_25, 2019.

BibTeX

@inproceedings{2019_nfm_stfmmr,
  title = {A Mixed Real and Floating-Point Solver},
  author = {Rocco Salvia and Laura Titolo and Marco A. Feliú and Mariano M. Moscato and César A. Muñoz and Zvonimir Rakamaric},
  booktitle = {Proceedings of the 11th NASA Formal Methods Symposium (NFM)},
  series = {Lecture Notes in Computer Science},
  volume = {11460},
  publisher = {Springer},
  editor = {Julia Badger and Kristin Yvonne Rozier},
  pages = {363--370},
  doi = {10.1007/978-3-030-20652-9_25},
  year = {2019}
}

Acknowledgements

Partially supported by NSF awards CCF 1346756 and CCF 1704715. Research by the first four authors was supported by the National Aeronautics and Space Administration under NASA/NIA Cooperative Agreement NNL09AA00A.

Abstract

Citation

BibTeX

Acknowledgements

Resources