Exploring Locally Bounded Translation Validation
summary
Extends Alive2 to accept local unroll bounds and formalizes locally bounded program pairs as a lattice, then uses random sampling with a search-and-prune strategy to avoid the code blowup that global unrolling causes. Experiments run with per-query 10s timeouts and an upper unroll of 15 on 119 TSVC functions show increased verification coverage versus Alive2’s global-bounds mode, producing concrete counterexamples where global unrolling times out.
AI-written summary · about
chapters (11)
- 0:00Locally bounded translation validation
- 1:23Why bounded translation validation
- 2:25Global vs local unroll bounds
- 4:09Local unroll bounds
- 5:56Global unroll bounds properties
- 6:59Partial order in local bounds
- 7:41Lattice search strategy
- 9:27Randomized lattice exploration
- 10:11Evaluation on TSVC
- 12:42Limitations and future work
- 13:05Q&A
related talks
18mA Verified Compiler for a Functional Tensor Language
15mInterleaving Large Language Models for Compiler Testing
11mFormally Verifying YUL Level Static Analyses and Optimization with Coq
53mFrom Within: Compiler Testing and Validation via Compilers
16mCounterexample-Guided Correlation Algorithm for Translation Validation
18mTowards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…)
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
18mDeveloping a Dependently Typed Language with Runtime Proof Search