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

TL;DR

Efficient Ranking Function-Based Termination Analysis with Bi-Directional Feedback introduces Syndicate, a framework that jointly synthesizes ranking functions and loop invariants via bi-directional feedback between Generate (ranking-function search) and Refine (invariant refinement) phases. By representing the program state with a meet-semilattice over annotated programs and using SMT-based sub-procedures, Syndicate achieves relative completeness under suitable templates and bounds the search by the depths of the invariant and ranking-function lattices, improving efficiency over monolithic approaches. Empirically, Syndicate proves more benchmarks with less average time than state-of-the-art tools across 168 challenging benchmarks, including cases where other tools fail, illustrating the practical impact of synergistic search in termination analysis. The framework is instantiated with flexible templates for $\mathcal{F}$ and $\mathcal{I}$ and supports nested and sequential loops, offering a versatile and scalable approach to automatic termination proofs.

Abstract

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.

Figures (16)

• Figure 1: For a single loop, we maintain $r, \mathsf{I}$ as canonical representations of $t, \mathsf{A}_{\mathsf{L}}$ respectively. First, we use the set $r$ to generate a candidate ranking function and then use the invariant $\mathsf{I}$ to check the validity. If we get a counterexample $p$, we try to refine the invariant $\mathsf{I}$ to exclude $p$. If $p$ is not reachable, the invariant is refined successfully to $\mathsf{I}'$ (green arrow). Otherwise (red arrow), we add $p$ to the set $r$. In both cases, the reachable states discovered while trying to refine $\mathsf{I}$ (denoted by $q$), are also added to the set $r$.
• Figure 2: Example terminating program
• Figure 3: Number of benchmarks out of 168 proved by Syndicate and baselines for different templates.
• Figure 4: Nested loop program
• Figure 5: Assume that $\mathsf{A}^*$ can prove the validity of $f$. Since $\mathsf{A}' \preceq \mathsf{A}$, $\mathsf{A}$ can be refined to $\mathsf{A}'$, which can also prove the validity of $f$.

Theorems & Definitions (15)

• Definition 3.1: Correctness of a Ranking Function
• Proposition 3.1
• Lemma 4.1
• Lemma 4.2
• Theorem 4.1: Soundness
• Theorem 4.2: Completeness
• Definition A.1
• Definition A.2
• Lemma B.1
• Lemma B.2