Exact Loop Bound Analysis
summary
Tool computes exact iteration counts for single-loop Linear Integer Arithmetic programs by synthesizing precondition synthesis fragments and reducing each case to a safety check. Implementation Elba uses Z3 for SMT solving and a safety verifier (Freeorn), and produces a loop-free bound function per case. Evaluation returns 62 of 75 benchmarks with exact bounds, typically under 20 seconds, and is limited today to deterministic, linear-variable loops (no linked lists or nonlinear bounds).
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:26Beyond upper and lower limits
- 2:29High-level approach
- 4:18Augmenting programs with counters
- 6:03Local bound discovery
- 8:33Precondition synthesis
- 10:40Verifying bounds
- 11:23Iterative search
- 12:49Elba tool architecture
- 13:36Implementation and results
- 15:45Summary and future work
- 17:07Q&A: Bound function
- 18:13Q&A: Loop characterization
- 19:17Q&A: Data structures
- 20:00Q&A: Linear vs nonlinear bounds
related talks
19mBeyond Affine Loops: A Geometric Approach to Program Synthesis
22mExecution Time Program Verification With Tight Bounds
23mSpecifying and Verifying Future Conditions
59mUnder-approximation for Scalable Bug Detection
13mBackward Symbolic Execution with Loop Folding
50mRecent Advances in Floating-point (Static) Analyses
15mData-Driven Abductive Inference of Library Specifications
01h 05mVerifying Infinitely Many Programs at Once