2 citations · 2 across the 3 of their papers we have counts for
Showing 2022Show all
2 papers · 1 filter
cs.LO2022
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…
cs.LO2022★ 2 cited
Extracting efficient exact real number computation from proofs in constructive type theory
Michal Konečný, Sewon Park, Holger Thies
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When prov…