Lifted Termination Analysis by Abstract Interpretation and its Applications

on YouTube ↗14m

" summary

A lifted termination analyzer, SPLFuncTion, implements a lifted decision tree domain on top of the FuncTion single‑program analyzer (OCaml, APRON numeric domains) and proves termination for #ifdef C families without enumerating every variant. The method synthesizes piecewise affine ranking functions, compacts eight‑variant examples into three shared leaves, and speeds analysis versus tuple lifting (often orders of magnitude) while handling termination‑directed sketching (timeouts drop for 8‑bit holes). Benchmarks on SV‑COMP loops show equal precision and markedly better performance.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 2:25Termination in program families
3. 3:15Brute force vs variability encoding
4. 5:06Tuple-based limits
5. 6:52Decision trees for efficiency
6. 8:08Termination-directed sketching
7. 9:35Formalization
8. 10:44Lifted abstract operations
9. 12:01Implementation results
10. 13:14Sketching performance
11. 14:01Conclusion