Automatic Inference of Ranking Functions by Abstract Interpretation


We present a family of parameterized abstract domains for proving termination of imperative programs by abstract interpretation. The domains automatically synthesize piecewise-defined ranking functions and infer sufficient conditions for program termination. We have implemented a prototype static analyzer for proving termination of programs written in (a subset of) C and, using experimental evidence, we show that it is competitive with the state of the art and performs well on a wide variety of benchmarks.

🇫🇷 INRIA Paris-Rocquencourt, France