Floating-Point TVPI Abstract Domain
summary
TVPI-FP implements a two-variables-per-inequality abstract domain that allows interval coefficients to model floating-point roundoff, supports branches, loops and elementary functions, and is implemented using floating-point arithmetic. Evaluation on 62 benchmarks shows an average 1.46 improvement factor over the box baseline; it is often 1–4 orders of magnitude faster than SMT-based DA tools but about 4.6× slower than Fluctuat, and uses a TVPI-style widening that trades precision for convergence.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:25Numerical abstract domains
- 2:26TBPI abstract domain
- 3:09Rounding errors in constraints
- 4:37TVPI-FP with intervals
- 6:05Non-convex inequalities
- 8:19Unknown states in arithmetic
- 11:34Evaluation and benchmarks
- 13:44Accuracy vs runtime trade-offs
- 14:46TVPI-FP contributions
- 15:07Q&A
related talks
48mDemystifying Floating Point
17mMiniFloat-NN: A RISC-V ISA Extension for Low-Precision NN Training
19mSolving Floating-Point Constraints with Continuous Optimization
50mElevating Precision in C++ - A Journey Below the Surface of Floating-Point
12mMixPert: Optimizing Mixed-Precision Floating-Point Emulation on GPU Integer Tensor Cores
10mSupport TVM QNN Flow on RISC-V with SIMD Computation
26mLow-Precision Inference without Quality Loss...
14mFast Linear Programming through Transprecision Computing on Small and Sparse Data