Counterexample- and Simulation-Guided Floating-Point Loop Invariant Synthesis

on YouTube ↗20m

" summary

Method synthesizes floating-point loop invariants by combining counterexample-guided synthesis with random simulation and a noisy polynomial fit for candidate ellipsoids, abstracting rounding with Daisy and verifying with reals before checking floats. Implemented as Pine, it handles all 6 non-linear benchmarks, yields invariants 12.4× tighter on average for linear cases, confirms real invariants as floating-point in 97% of runs, runs in ~25s average, and needs generalization from counterexamples in 92% of successful configs.

AI-written summary · about

" chapters (20)

1. 0:00Intro
2. 0:19Floating-Point Loop Invariants property I that holds on loop entry
3. 1:12Inductive Floating-Point Loop Invariants
4. 2:16Verifying Inductive Loop Invariants
5. 2:36Finding Floating-Point Loop Invariants
6. 4:00Challenges
7. 4:45Key Ideas
8. 5:18Counterexample Guided Inductive Synthesis CEGIS
9. 6:00Our Approach
10. 6:54Initialization
11. 7:31Candidate Invariant Generation - compute convex hul
12. 8:39Invariant Verification
13. 9:58Generalization from Counterexamples
14. 12:10Generate Next Candidate
15. 12:33Convergence
16. 12:55Implementation - Pine
17. 14:08Experimental Evaluation - Pine
18. 15:14Comparison to Other Tools
19. 17:16Parameter Sensitivity
20. 19:03CEGIS for Floating-Point Loop Invariants