Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers.

Junaid Rasheed Michal Konecný

Published in: SEFM (2022)

Keyphrases

floating point
fixed point
square root
instruction set
model checking
sparse matrices
floating point arithmetic
three dimensional
image sequences
dynamic programming
general purpose
theorem proving
interval arithmetic
hardware designs