Inferring loop invariants of programs with polynomial post-conditions
Mengjun Li · 2014
Based on the term dropping heuristics and dynamic approach, this paper presents a practical approach to infer loop invariants of programs with polynomial post-conditions, the inferred invariants include both the polynomial equality loop invariants and the polynomial inequality loop invariants. The effectiveness of the approach is demonstrated on examples.