Abstract
When compared to idealized, real-valued arithmetic, finite precision arithmetic introduces unavoidable errors, for which numerous tools compute sound upper bounds. To ensure soundness, providing formal guarantees on these complex tools is highly valuable. In this paper we extend one such formally verified tool, FloVer. First, we extend FloVer with an SMT-based domain using results from an external SMT solver as an oracle. Second, we implement interval subdivision on top of the existing analyses. Our evaluation shows that these extensions allow FloVer to efficiently certify more precise bounds for nonlinear expressions.
Author supplied keywords
Cite
CITATION STYLE
Bard, J., Becker, H., & Darulova, E. (2019). Formally verified roundoff errors using SMT-based certificates and subdivisions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11800 LNCS, pp. 38–44). Springer. https://doi.org/10.1007/978-3-030-30942-8_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
