@entry{bar-bec-dar-19-aa-smt, author = {J Bard and H Becker and E Darulova}, title = {Formally verified roundoff errors using SMT-based certificates and subdivisions}, journal = {International Symposium on Formal ...,}, volume = {}, number = {}, pages = {}, year = 2019, month = , doi = {}, comment = {}, abstract = {}, url = {{\url{https://link.springer.com/chapter/10.1007/978-3-030-30942-8_4}}}, quotes = {... Verifying SMT-based results also allowed us to compute and verify a roundoff error for the JetEngine benchmark, for which interval and affine arithmetic report a spurious division by ...} }