Efficient Ranking Function-Based Termination Analysis Via Bidirectional Decompositional Search

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. Since the set of reachable states is unknown, loop invariants are used to over-approximate it, requiring the joint synthesis of ranking functions and invariants. Existing approaches either synthesize them independently, encode them into a single monolithic query, or connect them through ad hoc, one-way information flow, leading to inefficient exploration of large search spaces. We present Syndicate, a termination analysis framework based on the novel concept of Bidirectional Decompositional Search (BDS). BDS keeps the ranking function and invariant synthesis decomposed but ensures continuous bi-directional feedback. This mutual guidance enables efficient exploration, significantly increasing the number of programs proven to terminate while reducing runtime compared to baselines without such feedback. Depending on the templates used, Syndicate is both relatively complete and provably efficient, outperforming existing techniques that achieve at most one of these guarantees. Despite its simplicity, Syndicate matches or surpasses state-of-the-art tools in termination proofs and runtime, demonstrating the effectiveness of bi-directional reasoning in termination analysis. Github: https://github.com/uiuc-focal-lab/Syndicate