Auto-active Verification of Floating-point Programs via Nonlinear Real Provers

Junaid Rasheed, Michal Konečný

We give a process for verifying numerical programs against their functional specifications. Our implementation is capable of automatically verifying programs against tight error bo…