Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback

Synthesizing ranking functions is a common technique for proving the termination of loops. A ranking function must be bounded and decrease by a specified amount with each iteration for all reachable program states. However, the set of reachable program states is often unknown, and loop invariants are typically used to overapproximate it. So, proving the termination of a loop requires searching for both a ranking function and a loop invariant. Existing ranking function-based termination analysis techniques can be broadly categorized as (i) those that synthesize the ranking function and invariants independently, (ii) those that combine invariant synthesis with ranking function synthesis into a single query, and (iii) those that offer limited feedback from ranking function synthesis to guide invariant synthesis. These approaches either suffer from having too large a search space or inefficiently exploring the smaller, individual search spaces. In this work, we present a novel termination analysis framework Syndicate, which exploits bi-directional feedback to guide the searches for both ranking functions and invariants, increasing the number of programs that can be proven to terminate and reduces the average time needed to prove termination compared to baselines. Syndicate is general and allows different instantiations of templates, subprocedures, and parameters, offering users the flexibility to optimize the ranking function synthesis. Depending on the templates used, Syndicate is relatively complete and efficient, outperforming existing techniques that achieve at most one of these guarantees. Notably, despite a simpler approach compared to the baselines, Syndicate's performance is either comparable to or better than existing tools in terms of the number of benchmarks proved and average runtime.