VCFloat2: Floating-point error analysis in Coq
summary
VCFloat2 is a Coq tool that automatically and soundly computes floating‑point round‑off error bounds with computational reflection, handling nonstandard formats (double‑double), user‑defined externals (sin, cos) and proofs for exact‑division cases. It adds an efficient multinomial simplifier and a decomposition tactic to make interval solving feasible; on standard benchmarks it produces competitive bounds (example: error < 1/4,000,000 for a time‑step integrator) and generates verifiable certificates in about 10s, outperforming prior Coq workflows.
AI-written summary · about
chapters (21)
- 0:00VCFloat2 and verification goals
- 1:50Floating-point error analysis matters
- 3:13Harmonic oscillator integration
- 5:26Floating-point arithmetic errors
- 7:12Tools and VCFloat2 motivation
- 8:16VCFloat1 to VCFloat2 evolution
- 10:03Writing functional models
- 12:11Proving error bounds in Coq
- 13:16Interval arithmetic challenges
- 15:26Multinomial simplifier for proofs
- 16:53Non-polynomial formulas
- 18:20Plugging external functions
- 19:24Non-standard floating-point formats
- 21:55Benchmarking tools
- 23:43Summary and future directions
- 24:09Q&A: Tensor computations
- 25:15Q&A: Matrix-vector multiplication
- 26:19Q&A: Summation order errors
- 27:43Q&A: Batch summation reduction
- 28:26Q&A: Improving Coq simplifiers
- 29:52Q&A: Runtime analysis
related talks
16mVerifying Out-Of-Order RISC-V Vector Extension With Open Source Tools
21mCocotb as a comprehensive verification platform
12mRISC-V: Hardcore/Softcore Co-Simulation Environment with Cycle-Accurate Rollback
24mVerifying All the Flexibility of RISC-V within SoC DV Test Plans
16mAutomatic Test Generation and Verification for RISC-V Vector Extension
41m0Flake - Reaching reliable non-flaky tests
21mCombined Dynamic and Formal Verification Approach to Processor Verification
16mcocotb 2.0: celebrating 12 years of verification fun