A three-tier strategy for reasoning about floating-point numbers in SMT

DOI10.1007/978-3-319-63390-9_22zbMath1494.68282OpenAlexW2638593226MaRDI QIDQ2164244

Mohamed Iguernlala, Clément Fumex, Kailiang Ji, Sylvain Conchon, Guillaume Melquiond

Publication date: 12 August 2022

Full work available at URL: https://hal.inria.fr/hal-01522770/file/main.pdf

zbMATH Keywords

floating-point arithmeticSMTprogram verification

Mathematics Subject Classification ID

Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical algorithms for computer arithmetic, etc. (65Y04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Computer-assisted verification of four interval arithmetic operators ⋮ An SMT theory of fixed-point arithmetic

This page was built for publication: A three-tier strategy for reasoning about floating-point numbers in SMT