Auto-Active Verification of Floating-Point Programs via Nonlinear Real Provers. - Junaid Rasheed; Michal Konecný (SEFM, 2022)