@inproceedings{bar-bec-dar-19-aa-smt,
  author = {Bard, Joachim and Becker, Heiko and Darulova, Eva},
  title = {Formally Verified Roundoff Errors using {SMT}-based Certificates and Subdivisions},
  booktitle = {Formal Methods - The Next 30 Years: Proccedings of the 2019 International Symposium on Formal Methods (FM)},
  year = 2019,
  month = oct,
  location = {Oporto, PT},
  pages = {38–44},
  series = {Lecture Notes in Computer Science},
  volume = {11800},
  doi = {10.1007/978-3-030-30942-8_4},
  comment = {Estimating roudoff and overflow errors in DSP. Says that the popular FloVer tool uses AA. Proposes a Satisfiability Modulo Theory (SMT) based range estimator that tracks non-linear correlations. Claims it is better than IA and AA, that ``report a spurious division by zero error'' (?).},
  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.}
}