#  Syndicate: Synergistic Synthesis of Ranking Function and Invariants for
Termination Analysis

Yasmin Sarita  University of Illinois Urbana-ChampaignUSA
<EMAIL_ADDRESS>,  Avaljot Singh  University of Illinois Urbana-
ChampaignUSA<EMAIL_ADDRESS>,  Shaurya Gomber  University of Illinois
Urbana-ChampaignUSA<EMAIL_ADDRESS>,  Gagandeep Singh  University of
Illinois Urbana-Champaign and VMware ResearchUSA<EMAIL_ADDRESS>and
Mahesh Vishwanathan  University of Illinois Urbana-ChampaignUSA
<EMAIL_ADDRESS>
###### Abstract.

Several techniques have been developed to prove the termination of programs.
Finding ranking functions is one of the common approaches to do so. A ranking
function must be bounded and must reduce at every iteration for all the
reachable program states. Since the set of reachable states is often unknown,
invariants serve as an over-approximation. Further, in the case of nested
loops, the initial set of program states for the nested loop can be determined
by the invariant of the outer loop. So, invariants play an important role in
proving the validity of a ranking function in the absence of the exact
reachable states. However, in the existing techniques, either the invariants
are synthesized independently, or combined with ranking function synthesis
into a single query, both of which are inefficient.

We observe that a guided search for invariants and ranking functions can have
benefits in terms of the number of programs that can be proved to terminate
and the time needed to identify a proof of termination. So, in this work, we
develop Syndicate, a novel framework that synergistically guides the search
for both the ranking function and an invariant that together constitute a
proof of termination. Owing to our synergistic approach, Syndicate can not
only prove the termination of more benchmarks but also achieves a reduction
ranging from 17% to 70% in the average runtime as compared to existing state-
of-the-art termination analysis tools. We also prove that Syndicate is
relatively complete, i.e., if there exists a ranking function and an invariant
in their respective templates that can be used to prove the termination of a
program, then Syndicate will always find it if there exist complete procedures
for the template-specific functions in our framework.

Termination, Program Analysis, Verification, Ranking functions, Invariants

††copyright: acmlicensed††journal: JACM††journalvolume: 37††journalnumber:
4††article: 111††publicationmonth: 8††copyright: none††ccs: Software and its
engineering Formal software verification††ccs: Theory of computation Program
verification

##  1\. Introduction

Termination analysis is one of the most challenging components of program
verification. Several techniques for automatically proving termination or non-
termination have been explored in the past. These include using various
reduction orders, finding recurrent sets, fixpoint logic solving, etc, within
static or dynamic analyses or a combination of both (Giesl et al., 2017;
Heizmann et al., 2014; Le et al., 2020; Unno et al., 2023). One of the most
common techniques to prove the termination of programs and also the focus of
this work is finding ranking functions. Ranking functions have the property
that for all reachable states, they are bounded from below and decrease by at
least a certain amount in each iteration. This poses a problem because
computing the exact set of reachable states is undecidable. To overcome this,
loop invariants are typically used as an over-approximation of the reachable
states. So, to prove the termination of a program, there are two unknowns -
the ranking function and the loop invariant. However, synthesizing both
ranking functions and loop invariants together is challenging. Compared with
classical property-guided synthesis (Welp and Kuehlmann, 2014; Bradley, 2011),
we do not have direct access to the target property (a ranking function or an
invariant). Instead, we only know constraints on the target properties, i.e.,
the ranking function must be bounded and must reduce on all reachable states,
and the invariants must subsume the initial program states and must be
inductive.

Some existing termination analysis techniques like (Giacobbe et al., 2022; Le
et al., 2020) handle the above issue by synthesizing the invariants and
ranking functions independently and work by either hard-coding some candidate
invariants or outsourcing the invariant generation to an external solver. Due
to this independence, these techniques frequently spend a significant amount
of time in discovering invariants that are either not useful to prove
termination or are stronger than necessary. Techniques like (Cook et al.,
2006) use their current set of ranking functions to guide a binary
reachability analysis procedure. However, this procedure is done using an
external temporal safety checker, so insights gained during one call to the
safety checker cannot be used to guide the ranking function generation
procedure or future calls to the safety checker. On the opposite side of the
spectrum, methods such as (Unno et al., 2021) pose the synthesis of ranking
functions and an over-approximation of the reachable states into a task of
verifying the satisfiability of a formula in fixpoint logic. This tightly
couples both tasks, making the search space for the combined query a
significantly large product of their individual search spaces.

Synergy. We argue that for a given program with a single loop, although the
search for ranking functions and the corresponding invariants must not be
agnostic of each other, directly encoding them as a monolithic query can make
each step of the search expensive. So, we propose that they should still be
searched using separate subroutines, but both sub-routines must exchange key
information with each other. Suppose the ranking function generated by the
ranking function synthesizer is invalid. In that case, the generated counter-
example can be used in one of these two ways: (1) if the counter-example is
not a reachable program state, it can guide the invariant synthesizer toward a
new invariant that excludes the counter-example, or (2) if the counter-example
is reachable and we find that no possible invariant can exclude it, this
search for a possible invariant will enable the discovery of new program
states that are conclusively reachable. These states then guide the search for
a new candidate ranking function. Since both the searches guide each other
with the common goal of finding a valid termination argument, this synergy
enables an efficient search for a ranking function and an invariant that is
just strong-enough to prove termination. Synergistic search of ranking
function and invariant synthesizers is computationally efficient, thus
allowing the advantages of both sides of the spectrum while minimizing their
drawbacks.

Multiple Loops. Proving the termination of programs with multiple loops
(nested or sequential) adds another level to the problem’s difficulty. All the
loops in the program must terminate, however, the search for ranking functions
and corresponding invariants cannot be independent across different loops. For
instance, in the case of nested loops, the invariant of the outer loop defines
the over-approximation of the initial set of the inner loop. So, the precision
of the outer invariant affects the inner loop’s invariant and ranking
function. Conversely, the inner invariant describes the over-approximated
transition relation of the outer loop’s body and thus affects the search for
the outer loop’s invariant and ranking function. Also, as expected, it is
inefficient to encode the search for all the invariants and the ranking
functions as a single query because of the prohibitively large search space,
and it may not even be needed in most cases. To address this problem, in
addition to having synergy between the searches for a ranking function and
invariant for one loop, we must also use the information from the invariant
search in each loop to guide the searches for ranking functions and invariants
of other loops in the program.

This Work. We introduce a new, general, framework called Syndicate, based on a
synergistic synthesis of ranking functions and invariants for efficient
termination analysis of complex programs containing arbitrarily nested loops,
disjunctive conditionals, and non-linear statements. Syndicate is data-driven
and synthesizes ranking functions from execution traces which makes it less
dependent on the exact structure of the loop. It is parameterized by a set of
possible invariants $\mathcal{I}$ and a set of possible ranking functions
$\mathcal{F}$ and can be instantiated with different choices of these sets to
obtain different termination analyses. For each loop, counter-examples from
the invariant search guide the ranking function search, and counter-examples
from the ranking function search guide the invariant search. Further, the
invariant and ranking function searches for each loop are guided by the
analyses of the other loops in the program. Under computability assumptions
and assumptions on the structure of $\mathcal{I}$ and $\mathcal{F}$, we
guarantee completeness: for a given program $P$, if there is a termination
proof using the invariants in $\mathcal{I}$ and ranking functions in
$\mathcal{F}$, then Syndicate will find a ranking function $f\in\mathcal{F}$
that is valid under an invariant $\mathsf{I}\in\mathcal{I}$ for every loop in
$P$.

Main Contributions:

  * •

We provide a general recipe for the synergistic synthesis of invariants and
ranking functions in the form of a framework called Syndicate, which can be
instantiated with different templates for ranking functions and invariants. To
do this, we introduce annotated programs with which we build the necessary
formalism needed for synergistic search. Syndicate handles complex programs
with arbitrarily nested and sequential loops, disjunctive conditionals, and
non-linear statements.

  * •

We show an additive upper bound on the number of iterations in terms of the
depths of lattices of invariants and ranking functions, while also
guaranteeing the soundness and relative completeness of Syndicate.

  * •

We provide an implementation of Syndicate and evaluate it on challenging
benchmarks (Beyer, 2020; Giesl et al., 2019; Giacobbe et al., 2022). Our
results show that we outperform state-of-the-art termination analysis tools
(Giacobbe et al., 2022; Giesl et al., 2017; Le et al., 2020; Heizmann et al.,
2014) both in the number of benchmarks proved and in the average time. We also
prove some benchmarks that none of these analysis tools can prove.

##  2\. Overview

We aim to find a ranking function $f$ for a loop program
$\mathsf{L}=\texttt{while}(\beta)\texttt{ do }\mathsf{P}_{1}\texttt{ od}$ in
some program $\mathsf{P}$. We use $\mathcal{R}$ to refer to the set of
reachable program states at the beginning of the loop and
$\llbracket\mathsf{P}_{1}\rrbracket$ to refer to the relation that captures
the semantics of the loop body $\mathsf{P}_{1}$. Note that $\mathsf{P}_{1}$
can itself have loops. A function $f$ is a valid ranking function for the loop
program $\mathsf{L}$ w.r.t $\mathcal{R},\llbracket\mathsf{P}_{1}\rrbracket$ if
it is bounded for all states in $\mathcal{R}$ and reduces for all pairs of
states in $\llbracket\mathsf{P}_{1}\rrbracket$.

  1. (1)

Bounded:  $\forall s\in\mathcal{R}\cdot f(s)\geq 0$

  2. (2)

Reducing:  $\forall(s,s^{\prime})\in\mathsf{P}_{1}\cdot f(s)-f(s^{\prime})\geq
1$

Typically, ranking functions are only required to be bounded above some value
(say $\theta$) and decrease by some minimum amount (say $\delta$). However, if
a ranking function $g$ satisfying the more general properties exists, then a
ranking function bounded by 0 and reducing by at least one exists. At each
step of our algorithm, we maintain a state defined by a tuple $\langle
t,\mathsf{A}_{\mathsf{L}}\rangle$. $t\subseteq S\times S$ is a set of pairs of
states occurring at the start and end of the loop body, initially sampled by
executing the program on random inputs. $t$ serves as an under-approximation
of $\llbracket\mathsf{P}\rrbracket_{1}$ such that
$\mathsf{dom}(t)\subseteq\mathcal{R}$. The second part of the algorithm state,
$\mathsf{A}_{\mathsf{L}}$, stores the program as well as invariants associated
with each loop in the program. These invariants can be used to define an over-
approximation of the reachable states at each loop head. The loop body
transition relation can also be over-approximated using the loop invariant
$\mathsf{I}$ and the loop guard $\beta$ as
$\mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket)$. We define the
structure,
$\mathsf{A}_{\mathsf{L}}=\mathsf{I}\;@\;\texttt{while}(\beta)\texttt{ do
}\mathsf{A}_{1}\texttt{ od}$, as an annotated program, where each loop in the
program is annotated by its invariant. Sematics of any program $\mathsf{P}$,
$\llbracket\mathsf{P}\rrbracket$, can then be over-approximated using the
invariants in the annotated program $\mathsf{A}$. This over-approximation is
denoted by $\llbracket\mathsf{A}\rrbracket$. We define annotated programs
formally in Section 4.

We present Syndicate which iteratively generates a candidate ranking function
$f$ and then refines the state of the algorithm until the generated candidate
is proven to be valid. We can generate a candidate ranking function by finding
a function that satisfies the Bounded and Reducing properties on the states in
$t$ since $t$ is an under-approximation of
$\llbracket\mathsf{P}\rrbracket_{1}$ and
$\mathsf{dom}(t)\subseteq\mathcal{R}$.

(1) $\forall(s,s^{\prime})\in t\cdot\big{(}f(s)-f(s^{\prime})\geq
1\big{)}\wedge\big{(}f(s)\geq 0\big{)}$

We then check the validity of the ranking function using
$\mathsf{A}_{\mathsf{L}}$.

(2)
$\forall(s,s^{\prime})\in\llbracket\mathsf{A}_{\mathsf{L}}\rrbracket\cdot(s\in\llbracket\beta\rrbracket)\implies(f(s)-f(s^{\prime})\geq
1\wedge f(s)\geq 0)$

If we cannot prove the validity of the ranking function, we obtain a counter-
example $(p,p^{\prime})$ on which either the Bounded or Reducing property is
not satisfied. Using this counter-example, we refine the state of our
algorithm. At this point, there can be two possibilities - (i) $p$ is not a
reachable state, which implies that the invariant $\mathsf{I}$ is weak, or
(ii) $f$ is invalid. We first try to refine the invariant to exclude the
counterexample $(p,p^{\prime})$. This is further done in two steps which are
explained later in this section. If we can refine the invariant, we update
$\mathsf{A}_{\mathsf{L}}$ with a stronger invariant. If we cannot find an
invariant that excludes $(p,p^{\prime})$, then $(p,p^{\prime})$ is added to
the set $t$. In either case, we have a refinement of the algorithm state that
leads to a better approximation of the reachable states $\mathcal{R}$. The
process continues until we find a ranking function and an invariant that
constitute a valid proof of termination of $\mathsf{L}$. While trying to
refine the invariant, we may also encounter some reachable states
$\\{(q_{1},q^{\prime}_{1}),(q_{2},q^{\prime}_{2}),\cdots\\}$ that are not
already in $t$. These are also added to $t$ during the refinement of the
algorithm state. Note that the counter-example $(p,p^{\prime})$ guides the
search for an invariant that can prove the current candidate ranking function,
and the new reachable state pairs $\\{(q_{i},q_{i}^{\prime})\\}$ guide the
search for better candidate ranking functions in subsequent iterations of our
algorithm.

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 counter-example $p$, we try to
refine the invariant $\mathsf{I}$ to exclude $p$. If $p$ is not reachable, the
invariant is refined successfully. Otherwise, we add $p$ and $q$ (reachable
states discovered while trying to refine $\mathsf{I}$) to the set $r$.

In our algorithm we define $\mathcal{I}$ to be the set of possible invariants
we can use for a loop. Because of this, when we say a counter-example, $s$, is
reachable, we mean there is no valid invariant in $\mathcal{I}$ that excludes
$s$. Similarly, we define $\mathcal{F}$ to be the set of possible ranking
functions and we only synthesize ranking functions from this set.

###  2.1. Syndicate Through an Example

⬇

1 y = n;

2 z = n+1;

3 while (m+y >= 0 &&

4 m <= n)

5 {

6 m = 2 * m + y;

7 y = z;

8 z = z + 1;

9 }\end{lstlisting}

10 \caption{Example terminating program}

11 \label{overview:code3}

12 \end{minipage}

13 \hspace{0.4cm}

14 \begin{minipage}{0.6\textwidth}

15 \scriptsize

16 \begin{align*}

17 \qquad&\rf(m’, y’, z’, n’) \\\

18 &= \max\big(1-(m’+y’), 0\big) + \max(n’ - m’ + 1, 0) \\\

19 &= \max\big(1-2m-y-z, 0\big) + \max(n-2m-y+1,0) \\\

20 &= \max\big(1-2m-y-\fbox{\textbf{(y+1)}}, 0\big) +
\max\big(n-m+1-(m+y),0\big) \\\

21 &= \max(-2m-2y, 0) + \max\big(n-m+1-(m+y),0\big) \\\

22 &= 0 +\max\big(n-m+1-(m+y),0\big) \\\

23 &= \max\big(n-m+1-(m+y),0\big) \\\

24 &\leq \rf(m, y, z, n) - 1

25 \end{align*}

26 \caption{Value of Ranking function at the end of one iteration}

27 \label{overview:rankingred2}

28 \end{minipage}

29\end{figure}

30

31\begin{table}

32 \centering

33 \scriptsize

34 \resizebox{0.8\textwidth}{!}{

35 \begin{tabular}{@{}lrrrr@{}}

36 \hline

37 &$r$ & $\invar$ & $\rf$ & $cex$ \\\

38 \hline

39 1&$\\{(1,2,3,4),(2,2,3,4)\\}$ & $\true$ & $\max(n-m,0)$ & $(1,-1,2,4)$ \\\

40 % \multirow{2}{*}{1}&$\\{(1,2,3,4),$ & \multirow{2}{*}{$\true$} &
\multirow{2}{*}{$\max(n-m,0)$} & \multirow{2}{*}{$(1,-1,2,4)$} \\\

41 % &$(2,2,3,4)\\}$ & & & \\\

42 \hline

43 2&$\\{(1,2,3,4),(2,2,3,4)\\}$ & \textcolor{blue}{$y+1 \geq z$} &
$\max(n-m,0)$ & $(1,-1,-1,1)$ \\\

44 % \multirow{2}{*}{2}&$\\{(1,2,3,4)$ &
\multirow{2}{*}{$\textcolor{blue}{y+1\geq z}$} &
\multirow{2}{*}{$\max(n-m,0)$} & \multirow{2}{*}{$(1,-1,-1,1)$} \\\

45 % &$(2,2,3,4)\\}$ & & & \\\

46 \hline

47 \multirow{2}{*}{3}&$\\{(1,2,3,4),(2,2,3,4),$ &
\multirow{2}{*}{$\textcolor{blue}{(y+1\geq z) \wedge (y+1\leq z)}$} &
\multirow{2}{*}{$\textcolor{blue}{\max(n-m+1,0)}$} &
\multirow{2}{*}{$(1,-1,0,4)$} \\\

48 &$\textcolor{blue}{(1,1,2,1)}\\}$ & & & \\\

49 \hline

50 \multirow{2}{*}{4}&$\\{(1,2,3,4), (2,2,3,4), $ & \multirow{2}{*}{$(y\geq
z-1) \wedge (y\leq z-1)$} & $\textcolor{blue}{\max(n-m+1,0) + }$ &
\multirow{2}{*}{-} \\\

51 &$(1,1,2,1),\textcolor{blue}{(1,-1,0,4)}\\}$ & &
$\textcolor{blue}{\max(1-m-y, 0)}$ & \\\

52 \hline

53 \end{tabular}

54 }

55 \caption{Steps taken by \toolname to prove the termination for the program
in Fig.~\ref{overview:code3}}

56 \label{tab:overview1}

57\end{table}

58

59% \begin{wrapfigure}{l}{0.5\linewidth}

60%
\begin{lstlisting}[numbers=left,basicstyle=\ttfamily\footnotesize,backgroundcolor=\color{backcolour}]

61% y = n;

62% z = n+1;

63% while (m + y >= 0 && m <= n) {

64% m = 2 * m + y;

65% y = z;

66% z = z + 1;

67% }\end{lstlisting}

68% \caption{Example terminating program}

69% \label{overview:code3}

70% \end{wrapfigure}

71\noindent

72We show the working of \toolname on a terminating single-loop program in
Fig.~\ref{overview:code3}.

73% \mvcom{Maybe you mean Program in Fig.~\ref{overview:code3}?}

74% (taken from the benchmarks used in Section~\ref{sec:evaluation} \sgcom{I
remember me and Aval coming up with this to demonstrate the approach easily,
is it fine to write that this is from the benchmarks}).

75In each iteration, $z$ increases by 1, and as $y$ is set to the previous
iteration value of $z$, $y$ also increases by 1. For each iteration, $m+y\ge
0$ and $m\le n$ (from the loop guard). In each iteration, $m$ increases by $m
+ y$. There are two cases: (1) If $m + y > 0$ at the beginning of the first
iteration, then $m$ will increase in every iteration and eventually be greater
than $n$, and (2) If $m + y = 0$ at the beginning of the first iteration, $m$
stays constant for the first iteration, $y$ always increases (as noted above),
which means that after the first iteration, $m + y > 0$. So, $m$ increases on
every iteration after the first and eventually becomes greater than $n$. A
ranking function for this loop is $\max(n-m+1,0) + \max(1-m-y,0)$ because for
all reachable states, either $n-m+1$ is reducing and $1-m-y$ stays constant or
$n-m+1$ stays constant and $1-m-y$ reduces from 1 to 0. However, we need an
invariant $\inv \equiv y + 1 = z$

76% \mvcom{missing Fig.?}

77to prove its validity (Fig.~\ref{overview:rankingred2}).

78For the rest of this section, we refer to the program in
Fig.~\ref{overview:code3}

79% \mvcom{again this should be program in Fig. ..}

80as $\pgm$, and the loop-body (lines 6-8) as $\pgm_1$.

81

82% \begin{align*}

83% \qquad&\rf(m’, y’, z’, n’) \\\

84% &= \max\big(1-(m’+y’), 0\big) + \max(n’ - m’ + 1, 0) \\\

85% &= \max\big(1-2m-y-z, 0\big) + \max(n-2m-y+1,0) \\\

86% &= \max\big(1-2m-y-\fbox{\textbf{(y+1)}}, 0\big) +
\max\big(n-m+1-(m+y),0\big) \\\

87% &= \max(-2m-2y, 0) + \max\big(n-m+1-(m+y),0\big) \\\

88% &= 0 +\max\big(n-m+1-(m+y),0\big) \\\

89% &= \max\big(n-m+1-(m+y),0\big) \\\

90% &\leq \rf(m, y, z, n) - 1

91% \end{align*}

92% \sgcom{The fig shows the derivation of the rf value after the iteration,
not exactly that it reduces}.

93

94% As explained before, in the case of a single loop, we can omit $t, T$ from
the algorithm state to avoid redundancy as it is easy to capture the loop body
transition semantics $\bracs \pro$.

95In the case of a single loop, our algorithm is described in
Fig.~\ref{fig:overview},

96% \mvcom{missing reference. Also, if the figures are labelled ‘‘Fig.’’, you
should refer to them as ‘‘Fig.’’, and if they are labeled as ‘‘Figure’’ then
you should refer to them as ‘‘Figure’’.}

97where it suffices to store a set of states $r$ instead of pairs of states
$t$. This is because given a state $s$ at the beginning of a loop, the program
state $s’$ at the end of one iteration can be computed as $\bracs{\pgm_1} s$.
Similarly, instead of storing the annotated program $\annopgm$, we store the
invariant $\inv$ of the loop.

98%

99% In the case of a single loop, the annotated loop program $\alooppgm$
contains the loop program and its invariant. So, it suffices to store the
invariant of the loop ($\inv$) instead of $\alooppgm$ in the algorithm state.

100The set $r$ is initialized with randomly generated traces by running the
program $L$ for fixed iterations. Here, $r = \\{(1,2,3,4), (2,2,3,4)\\}$; a
program state is a tuple ($m, y, z, n$). The invariant is initialized with the
set of all states, i.e., $\invar = \true$. For this example, let $\tempr$, the
set of candidate ranking functions, be functions of the form $\max(a^1_0 +
\sum_j a^1_jx_j, 0) + \max(a^2_0 + \sum_j a^2_jx_j, 0)$ and $\tempi$, the set
of possible invariants, be conjunctions of constraints of the form $d_0 +
\sum_jd_jx_j \geq 0$, where $a^1_j,a^2_j,d_j \in \mathbb{Z}$ Note that our
algorithm can handle more general forms of ranking functions and invariants
that satisfy the conditions explained in Section~\ref{sec:theory}. Our
algorithm finds the ranking function and the corresponding invariant for this
example using separate queries, while also exchanging key information amongst
different phases in each iteration. This enables an efficient termination
analysis (Section~\ref{sec:efficiency}).

101% This leads us to achieve an improvement over the existing termination
analysis tools in terms of an upper bound on the number of iterations of the
CEGIS loops (Section~\ref{sec:efficiency}).

102% More detailed discussion on this can be found in
Section~\ref{sec:efficiency}.

103%

104The exact steps for our running example are explained below and also
displayed in Table~\ref{tab:overview1}.

105% in the following steps (as displayed in Table~\ref{tab:overview1}):

106% \mvcom{Why does Table~\ref{tab:overview1} appear before the program?}

107\myparagraph{Iteration 1} First, we get a candidate ranking function that
reduces for all states in $r$.

108Specifically, we find a satisfying assignment for the coefficients
$a^i_j$’s

109% \mvcom{$d_i$’s, perhaps?}

110that satisfy the following query.

111% based on Equation~\ref{eq:rfcreate}. \mvcom{This equation is 2 pages
back. We may need to add a page reference, if we need to refer to it. Or we
can just explain in words.}

112We do not have to check the bounded condition because all of the functions
of the template are bounded by 0.

113% We get the coefficients $a_i$s and $b_i$s for our ranking function
template by solving the following SMT query based on the semantics defined in
Equation~\ref{eq:rfcreate}:

114 \begin{gather*}

115 \forall (m,y,z,n) \in r \cdot \big( f(m,y,z,n) - f(\bracs{\pgm_1}
(m,y,z,n))\geq 1 \big)

116 \end{gather*}

117% where our template $f =\max(a_0 + \sum_i a_ix_i, 0) + \max(b_0 + \sum_i
b_ix_i, 0)$.

118We solve this query using Z3~\cite{z3} and obtain $f(m,y,z,n) =
\max(n-m+1,0)$.

119% Using the Z3 solver, we get the ranking function $f(m,y,z,n) =
\max(n-m+1,0)$.

120%

121Now, we check the candidate function’s validity w.r.t the current invariant
$\invar = \true$. This can be done by checking the satisfiability of the
following formula.

122% (based on the negation of Equation~\ref{eq:rfcheck}). \mvcom{same comment
about page reference for this equation. Also both equations are for the case
when the under-approximation is a set of pairs not a set of states.}

123\begin{gather*}

124 \forall (m,y,z,n) \cdot \big((m+y\geq 0) \wedge (m\leq n)\big) \implies
\big( f(m,y,z,n) - f(\bracs{\pgm_1} (m,y,z,n))\geq 1 \big)

125\end{gather*}

126% \begin{gather*}

127% (m,y,z,n) \in \inv \wedge \beta(m,y,z,n) \wedge \big(f(m,y,z,n) -
f(m’,y’,z’,n’) < 1\big), \quad \text{where} \\\

128% \beta(m,y,z,n) = (m+y \geq 0 \wedge m \leq n), \; f(m,y,z,n) =
\max(n-m+1,0)

129% % \\\ m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n

130% \end{gather*}

131% where $m, y, z, n$ are symbolic variables representing the literal state
at the beginning of the loop and $m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n$, which
are obtained by symbolically executing the loop body.

132Solving this gives a counter-example $p_1 = (1,-1,2,4)$.

133Next, we refine the algorithm state. There are two possibilities as
discussed above. Either $p_1$ is a reachable state and the ranking function is
invalid, or $p_1$ is not reachable. We first try to strengthen $\inv$ to
$\inv’$ s.t. $p_1 \notin \inv’$. This is done in 2 phases:

134

135

136% Next, first we try to find an invariant $\inv’$ that does not include
$c_1$ so that our counter-example pair $(c_1, c_1’)$ can be excluded. We
iteratively perform the two phases involved in refining the algorithm state.
\\\

137% Our algorithm does this by performing these two steps iteratively:\\\

138\myparagraph{Generate Invariant Phase} We generate a candidate invariant $
\inv’’$ that includes all states $s$ such that $s \in r$ and does not include
the state $p_1$. Here, $\rf$ tries to guide the refinement of an invariant
that can prove its validity. This is done by solving the following query for
the coefficients $d_j$ to get $\inv’’$ and then taking a conjunction with
$\inv$, i.e., $\inv’ = \inv’’ \wedge \inv$.

139\begin{gather*}

140 (1, -1, 2, 4) \notin \invar’’ \wedge \big( \forall (m,y,z,n) \in r \cdot
(m,y,z,n) \in \invar’’ \big) \\\

141 where \quad (m,y,z,n) \in \invar’’ \ \equiv \ d_0 + d_1m + d_2y + d_3z +
d_4n \geq 0

142\end{gather*}

143Solving the above query, we get $\inv’’ \equiv y-z+1 \geq 0$. We now
proceed to check the validity of $\inv’$.

144\myparagraph{Check Invariant Phase}

145The validity of the invariant $\invar’$ is checked by solving for a
counter-example for the following query.

146Here, $\ini$ is the set of states before the loop at line 3 executes.

147% \mvcom{$\init$ not given for this examples as far as I can tell.}

148\begin{gather*}

149 \big(\forall s \in \init, s \in \invar’\big) \wedge \big(\forall s \in \invar’ \implies \bracs{\pgm_1}s \in \invar’\big), \text{ where }\ini = \\{(m,y,z,n) | (y=n) \wedge (z=n+1)\\}

150\end{gather*}

151%

152% where $v$ represents symbolic variables generated to represent the state
before the loop body and $v’$ represents the values obtained after
symbolically executing the loop body on these variables.

153% If we do not get a counter-example, we have successfully refined the
invariant. Otherwise, we generate a new candidate invariant that removes this
new counter-example and check again until we either find a valid invariant or
get \texttt{unsat} while generating the invariant, in which case no such
invariant is possible.

154In our example, we do not get a counterexample, and hence, $y-z+1 \geq 0$
is a valid invariant.

155%

156As described above, we guide the invariant search to find an invariant that
excludes $p_1$. We update the algorithm state by changing $\inv$ to $\inv’$.
Since we store $\inv’$ in the algorithm state, future iterations of the
invariant generation phase in our algorithm will start with $\inv’$ instead of
$\true$ when trying to determine the reachability of another counter-example.
This is in contrast to algorithms~\cite{dynamite,terminator} that rely on
external solvers to find invariants because the external solvers do not have
information about the previous iterations.

157

158\myparagraph{Iteration 2}

159As the set $r$ is unchanged, we do not generate a new ranking function and
directly move on to checking the validity of the ranking function w.r.t the
new invariant.

160% the Generate Candidate phase generates the same function $r_f =
\max(n-m+1,0)$ and checks its validity w.r.t the new invariant $y + 1 \geq z$
to

161We get a new counter-example $p_2 = (1,-1,-1,1)$.

162% \mvcom{pair?}

163\myparagraph{Generate Invariant Phase} We try to strengthen our invariant
$y + 1 \geq z$ to exclude $p_2$ by generating a candidate invariants guided by
$p_2$. We generate the candidate $m-n-1 \ge 0$, which includes the states in
$r$ but excludes $p_2$.

164\myparagraph{Check Invariant Phase} When checking the validity of the new
invariant, we find the counter-example $q_2^1 = (1,1,2,1)$.

165% There are two types of counter-examples we can find when checking the
validity of a candidate invariant:

166% \begin{enumerate}

167% \item A pair of states, $(s,s’)$ such that $s \in \invar’$, $s \notin
\invar’$ and $s’ = \bracs \pgm s$

168% \item A state, $s$, in $\init$ that is not included in $\invar’$.

169% \end{enumerate}

170% In the first case, we go back to the Generate Invariant Phase and add the
additional constraint that for all future invariants generated, $I’’$,
$I’’(s_2) \implies I’’(s’_2)$. This condition prevents the same candidate
invariant from being generated twice.

171% The counter-example we obtained, (1,0,1,1), falls under the second case
because it is in $\init$ but not include in $\invar’$.

172Since $q_2^1 \in \init$,

173% \mvcom{can’t seem to find $\init$. Also, is this claim right? It seems
that when we start we have y=n and z=n+1. Isn’t the tuple $(m,z,y,n)$?}

174it is a reachable state. So, we can add it to $r$ to improve the under-
approximation of the reachable states. $q_2^1$ has a property that the other
states in $r$ do not, i.e., $m=n$. This guides the generation of candidate
ranking functions to reduce on states where $m=n$. Since the new invariant is
invalid, we go back to the Generate Invariant Phase with an additional
constraint that all candidate invariants should include $q_2^1$.

175 % Since the loop condition is true for this state, we can add
((1,0,1,1),(2,1,2,1)) to $t$. ((1,0,1,1),(2,1,2,1)) is a reachable pair of
states that has some property not found in any of the pairs of states in $t$,
so adding it to $t$ can guide the search for ranking functions by providing
diverse states to the under-approximation in the algorithm state. We then go
back to the Generate Invariant Phase and add the additional constraint that
for all future invariants generated, $I’’$, $(1,0,1,1) \in I’’$. This
condition prevents the same candidate invariant from being generated twice.

176After further iterations of finding and checking candidate invariants, we
get the invariant $y + 1 \geq z \wedge y + 1 \leq z$, which excludes $p_2$.

177\myparagraph{Iteration 3}

178The set $r$ is changed from the invariant search, so we generate a new
candidate ranking function. Guided by the state $q^1_2$, we get the ranking
function $\max(n-m+1,0)$. We check the validity of the ranking function w.r.t
the new invariant $y + 1 \geq z \wedge y + 1 \leq z$ to get a new counter-
example $p_3 = (1,-1,0,4)$. When refining the algorithm state, we are now
unable to find a valid invariant that excludes $p_3$ and thus we can conclude
that $p_3$ cannot be excluded from the set of reachable states using any
invariant from our template. So, we add it to $r$, refining the algorithm
state.

179\myparagraph{Iteration 4} As the set $r$ is updated, we generate a new
candidate ranking function $\rf = \max(n-m+1,0) + \max(1-m-y, 0)$ that reduces
on all states in the updated $r$. We then check its validity w.r.t the current
invariant $y + 1 \geq z \wedge y + 1 \leq z$. The validity check succeeds, and
$\rf = \max(n-m+1,0) + \max(1-m-y, 0)$ is returned as a valid ranking function
for the program.

180

181The above steps demonstrate the benefits of the synergistic approach in
finding a ranking function for the loop in Fig.~\ref{overview:code3} and an
invariant ($y + 1 = z$) that is useful for proving the validity of the ranking
function. Note that there are many valid invariants for this loop, such as $y
\leq z$, $y \geq n$, $z \geq n + 1$, etc. However, they do not help in finding
or proving the validity of the ranking function. The counter-examples found
when checking the validity of candidate ranking functions guide the search for
stronger invariants, as shown in iterations 1 and 2 above. Further, the
counter-examples found when checking the validity of candidate invariants
guide the search for a valid ranking function, as shown in iterations 2 and 3
above.

182

183\subsection{Nested Loops}

184\label{sec:nestedloops}

185\begin{wrapfigure}{l}{0.4\linewidth}

186\begin{lstlisting}[numbers=left,basicstyle=\ttfamily\footnotesize,backgroundcolor=\color{backcolour}]

187 y = n;

188 z = n+1;

189 while (y+n+1 >= k*k+z && y == z+1){

190 while (m+y >= 0 && m <= n){

191 m = 2*m + y;

192 y = z;

193 z = z+1;

194 }

195 y++;

196 z++;

197 n--;

198 }\end{lstlisting}

199\caption{Nested loop program}

200\label{fig:nest}

201\end{wrapfigure}

202\noindent

203When considering nested loops, instead of storing $r$, an under-
approximation of the reachable states, we have to store $t$, which contains
pairs of states, and serves as an under-approximation of the transition
relation of the loop because we can no longer directly compute the program
state at the end of the loop given the program state at the beginning.

204For instance, consider the program $\pgm$ in Fig.~\ref{fig:nest}.

205% \mvcom{reference number seems to be off.}

206$\pgm_i$ is the inner loop (lines 4-8),

207% \mvcom{is the loop body of the inner loop? If so should it be lines 5 to
7?},

208$\beta_o$ and $\beta_i$ are the loop guards at lines 3 and 4 respectively.
Given a program state $s$ before executing the inner loop at lines 4-8, we
cannot compute the state $s’$ just before line 9. This is because
$\bracs{\pgm_i}$ is also unknown. So, we use an invariant $\invar_i$ to over-
approximate $\bracs{\pgm_i}$. Similarly, we use an invariant $\invar_o$ for
the outer loop. Note that the initial set for $\invar_i$ depends on
$\invar_o$. Conversely, $\invar_o$ depends on $\bracs{\pgm_i}$ which is
approximated using $\invar_i$. So, the invariants corresponding to all the
loops in a program depend on each other.

209%

210Since we approximate the transition relation $\bracs{P}$ using a subset of
pairs of reachable states $t$, and the invariants ($\invar_i, \invar_o$), we
represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$.

211%

212While this algorithm state works for this example, it needs to be
generalized to programs with arbitrary nested or sequential loops. We achieve
this generalization using the notion of an annotated program, which is
discussed formally in Section~\ref{sec:annotatedpgm}.% For this example
(program in Fig.~\ref{fig:nest}), however, we use $\langle t, (\invar_o,
\invar_i) \rangle$ as the algorithm state.

213

214% In this setting, for the annotated program, $\alooppgm = \invar \; @ \;
\texttt{while}(\beta) \texttt{ do }\anno \texttt{ od}$, where $\anno$ also
contains loops. Consider the loop $L$ at line 3 in Fig.~\ref{fig:nest}. We
create a corresponding annotated program $\alooppgm$ where the invariants at
lines 3 and 4 are initialized as sets of all states, i.e., $\invar_o =
\invar_i = \true$.

215% Since we approximate the transition relation $\bracs{P}$ using a subset
of pairs of reachable states ($t$), and the invariants ($\invar_i, \invar_o$),
we represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$.
\mvcom{Earlier in the paper we use annotated program as the second component.
Here we are using a pair of invariants. Perhaps a holdover from old version of
the paper.}

216Note that here we will use the same templates $\tempr$ and $\tempi$ for
both loops, but this is not a requirement for our algorithm.

217Both invariants are initialized as the set of all states, i.e., $\invar_o =
\invar_i = \true$.

218Using this, we compute an initial set $\init_i$ for the inner program $\pgm_i$. In this case, $\init_i = \invar_o \cap \bracs{\beta_o} = \\{(m,y,z,n) | (y+n+1 \ge k*k+z) \wedge (y=z+1)\\}$. The initial set $\init_o$ for the outer while loop is $\\{(m,y,z,n) | (y=n) \wedge (z=n+1)\\}$.

219% \mvcom{Should we use $\init_o$ to be consistent with the rest of the
notation?}

220We can start by searching for a ranking function for either the outer or
inner loop first. We choose the inner loop. Since the body of the inner loop
is the same as the loop body in the program in Fig.~\ref{overview:code3} and
$\init_i$ is a subset of the $\init$ set we computed when analyzing the single
loop case, we can go through the same iterations as above to get $\rf_i =
\max(n-m+1,0) + \max(1-m-y, 0) $, $\invar_i \equiv y + 1 = z$, and $\invar_o =
\true$.

221% As the inner loop of the program is the same as the program in
Fig.~\ref{overview:code3}, we get $\rf_i = \max(n-m+1,0) + \max(1-m-y, 0) $,
$\invar_i = (y + 1 \geq z) \wedge (y + 1 \leq z) \equiv y + 1 = z$, and
$\invar_o = \true$.

222Next, \toolname uses similar steps as discussed in
Section~\ref{sec:example} to find a ranking function for the outer loop: \\\

223(1) We generate a candidate ranking function $\rf$ similar to the single
loop case. The one thing that changes while validating $\rf$ is that because
we have a loop in the body of the outer loop, we can not symbolically execute
to find the program state at the end of one iteration.

224% For e.g., consider that we have a candidate ranking function $\rf$ for
the outer loop along with the two invariants $\invar_o$ and $\invar_i$ and we
need to check its validity. We can no longer define symbolic variables
$m,y,z,n,k$ and do a symbolic execution of the loop body to get $m’, y’, z’,
n’, k’$ as we have the inner loop.

225To get through this, we define fresh variables $m’’, y’’, z’’, n’’, k’’$ to
represent the state just after the inner loop ends and assume that this state
satisfies $\invar_i \wedge \neg \beta_i$, and

226% \avcom{symbolic state?}

227% (where $\beta_i$ is the loop guard of the inner loop).

228% Using this, we

229define the validation query as:

230% We then analyze $\anno$ find valid invariants $\invar_i$ and $\invar_o$
and a ranking function $\rf_i$ that is valid w.r.t $\init$, $\invar_i$ and
$\invar_o$. We use $\invar_o$ to over-approximate the set of initial states
for the inner loop.

231% \textcolor{red}{Aval: previous line is unclear.}

232% Next, we try to find a ranking function for the outer loop.

233% For the outer loop, it is hard to compute the exact transition relation
of the loop body because the loop body itself has a loop. This makes it more
challenging to generate and check the validity of candidate ranking functions.

234% % To tackle this, our algorithm generates candidate ranking functions for
nested loops using samples from the execution traces ($t$), that serve as an
under-approximation of $\bracs \prog$ (where $\prog$ is the program at lines 4
to 11).

235% To check the validity of ranking functions, we use $\invar_i$ to over-
approximate $\bracs{\prog}$. Since we need both invariants for both loops,
while finding the ranking function for each loop, we can choose to refine
either $\invar_i$ or $\invar_o$ when we refine the algorithm state.

236% \textcolor{red}{Aval: Need to change the previous few lines. It is
repetition.}

237% To check the validity of ranking functions, we use the invariant
generated for the inner loop in $\anno$ to over-approximate the transition
relation induced by $\anno$ using the notion of $\bracs \anno$ (defined in
Section~\ref{sec:background}).

238

239

240\begin{table}

241 \centering

242 \resizebox{\textwidth}{!}{

243 \begin{tabular}{@{}lrrrr@{}}

244 \hline

245 &$t$ & $(\invar_o,\invar_i)$ & $\rf$ & $p, p’$ \\\

246 \hline

247 \multirow{2}{*}{1}&$\\{((2,2,3,4,1),(6,7,8,0,1)),$ &
\multirow{2}{*}{$(\true, y + 1 = z)$} & \multirow{2}{*}{$\max(n-k,0)$} &
\multirow{2}{*}{$(1,2,4,5,5), (7,2,3,5,5)$} \\\

248 &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

249 \hline

250 \multirow{2}{*}{2}&$\\{((2,2,3,4,1),(6,7,8,0,1)),$ &
\multirow{2}{*}{($\textcolor{blue}{y+1\geq z}, y+1=z)$} &
\multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,2,5,5), (8,3,4,5,5)$}
\\\

251 &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

252 \hline

253 \multirow{2}{*}{3}&$\\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{(

254 $\textcolor{blue}{(y+1\geq z) \wedge (y+1\leq z)}$, y + 1 = z)} &
\multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,3,5,5), (7,5,6,5,5)$}
\\\

255 &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

256 \hline

257 \multirow{3}{*}{4}&$\\{((2,2,3,4,1),(6,7,8,0,1)), $ &
\multirow{3}{*}{$((y\geq z-1) \wedge (y\leq z-1), y+1=z)$} &
\multirow{3}{*}{$\textcolor{blue}{\max(n-k+1,0)}$} & \multirow{3}{*}{-} \\\

258 &$((2,2,3,5,1), (6,8,9,0,1)),$ & & & \\\

259 &$\textcolor{blue}{((1,2,3,5,5),(7,5,6,5,5))}\\}$ & & & \\\

260 \hline

261 \end{tabular}

262 }

263 \caption{Steps taken by \toolname to prove the termination for the program
in Fig.~\ref{fig:nest}}

264 \label{tab:overview2}

265\end{table}

266

267% \begin{table}

268% \centering

269% \resizebox{\textwidth}{!}{

270% \begin{tabular}{@{}lrrrr@{}}

271% \hline

272% &$t$ & $(\invar_o,\invar_i)$ & $\rf$ & $p, p’$ \\\

273% \hline

274% 1&$\\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\\}$ & $(\true,
y + 1 = z)$ & $\max(n-k,0)$ & $(1,2,4,5,5), (7,2,3,5,5)$ \\\

275% % &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

276% \hline

277% 2&$\\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\\}$ &
$(\textcolor{blue}{y + 1 \geq z}, y + 1 = z)$ & $\max(n-k,0)$ & $(1,2,4,5,5),
(7,2,3,5,5)$ \\\

278% \hline

279% % \multirow{2}{*}{2}&$\\{((2,2,3,4,1),(6,7,8,0,1)),$ &
\multirow{2}{*}{($\textcolor{blue}{y+1\geq z}, y+1=z)$} &
\multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,2,5,5), (8,3,4,5,5)$}
\\\

280% % &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

281% % \hline

282% 3&$\\{((2,2,3,4,1),(6,7,8,0,1)),((2,2,3,5,1), (6,8,9,0,1))\\}$ &
$(\textcolor{blue}{(y + 1 \geq z)\wedge (y + 1 \leq z)}, y + 1 = z)$ &
$\max(n-k,0)$ & $(1,2,4,5,5), (7,2,3,5,5)$ \\\

283% \hline

284% % \multirow{2}{*}{3}&$\\{((2,2,3,4,1),(6,7,8,0,1)),$ & \multirow{2}{*}{(

285% % $\textcolor{blue}{(y+1\geq z) \wedge ((y+1\leq z)}$, y + 1 = z)} &
\multirow{2}{*}{$\max(n-k,0)$} & \multirow{2}{*}{$(1,2,3,5,5), (7,5,6,5,5)$}
\\\

286% % &$((2,2,3,5,1), (6,8,9,0,1))\\}$ & & & \\\

287% % \hline

288% \multirow{2}{*}{4}&$\\{(2,2,3,4,1),(6,7,8,0,1)), ((2,2,3,5,1),
(6,8,9,0,1)), $ & \multirow{2}{*}{$((y\geq z-1) \wedge (y\leq z-1), y+1=z)$} &
\multirow{2}{*}{$\textcolor{blue}{\max(n-k+1,0)}$} & \multirow{2}{*}{-} \\\

289% &$\textcolor{blue}{((1,2,3,5,5),(7,5,6,5,5)}\\}$ & & & \\\

290% \hline

291% \end{tabular}

292% }

293% \caption{Steps taken by \toolname to prove the termination for the
program in Fig.~\ref{fig:nest}}

294% \label{tab:overview2}

295% \end{table}

296

297

298

299

300% At each step, the algorithm state is defined by $\langle t, \anno_l
\rangle$.

301% The annotations of $A_l$ have the invariants for the two loops.

302% Since we approximate the transition relation $\bracs{P}$ using a subset
of pairs of reachable states ($t$), and the invariants ($\invar_i, \invar_o$),
we represent our algorithm state as $\langle t, (\invar_o, \invar_i) \rangle$.
$\invar_{o}$ and $\invar_i$ are initialized with the output obtained by
solving the inner loop ($\invar_i$).

303% Note that here we will use the same templates $\tempr$ and $\tempi$ for
both loops, but this is not a requirement for our algorithm.

304

305

306\begin{gather*}

307 \invar_o(m,y,z,n,k) \wedge \beta_o(m,y,z,n,k) \wedge \big(f(m,y,z,n,k) -
f(m’,y’,z’,n’,k’) < 1\big) \; \wedge \\\

308 \invar_i(m’’,y’’,z’’,n’’,k’’) \; \wedge \; \neg
\beta_i(m’’,y’’,z’’,n’’,k’’), \quad \text{where} \\\

309 % \beta_o(m,y,z,n,k) = (y+n+1 \geq k^2 + z), \quad
\beta_i(m’’,y’’,z’’,n’’,k’’) = (m’’+y’’ \geq 0 \wedge m’’ \leq n’’), \\\

310 m’ = m’’, \ y’ = y’’ + 1, \ z’ = z’’ + 1, \ n’ = n’’ - 1, \ k’ = k’’

311 % \\\ m’=2m+y, \ y’=z, \ z’=z+1, \ n’=n

312\end{gather*}

313\noindent

314(2) We refine the state of the algorithm. From the above validation query,
we get a counter-example of the form $(p, p’’, p’)$. Here $p$ and $p’$ are the
states at the beginning and end of one iteration of the outer loop, and $p’’$
is the state at the exit of the inner loop. So, the refine phase has two
options: (a) either refine the outer invariant $\invar_o$ first to exclude $p$
or (b) refine the inner invariant $\invar_i$ to exclude $p’’$. If at least one
of the invariants is refined, we check the validity of the ranking function
again. If it is not possible to refine either of the invariants, we add $(p,
p’)$ to t. Once we choose an invariant to refine, we iteratively go through
the Generate Invariant Phase and the Check Invariant Phase. If the invariant
we chose cannot be refined, we try to refine the other invariant.

315%

316Table~\ref{tab:overview2} gives the steps our algorithm takes to find the
ranking function for the outer loop.

317This approach can be generalized to nested loops with arbitrary depth as
explained in Section ~\ref{sec:theory}.

318% The approach described above can be generalized to any number of
nestings. Consider again a loop program of the form $\anno_l = \invar \; @ \;
\texttt{while}(\beta) \texttt{ do }\anno \texttt{ od}$. Our algorithm will
first prove the termination of all the loops present in $\anno$ and
simultaneously finds invariants for all of them. Once this is done, we can
then analyze $\anno_l$ using the invariants of the inner loops to over-
approximate the transition relation of $\anno$ using $\bracs \anno$. In the
refine phase in this case, either we refine the invariant of $\anno_l$ or at
least one of the inner loop invariants is refined to exclude the counter-
example sequence.

319

320% Say the program has $n$ nested loops $L_1, L_2, \cdots L_n$. Our
algorithm starts with the innermost loop $L_n$ and finds a ranking function
and an invariant ($I_n$) that validates it. We then shift to loop $L_{n-1}$.
In general, to prove the termination of loop $L_i$, we maintain a tuple of
invariants $(I_i, I_{i+1}, \cdots I_n)$ (one for each loop inside

321% and including $L_i$) that over-approximates the program transitions
($\trans$) and the set of reachable states of $L_i$. Then we iteratively try
to find a ranking function ($\rf$) from the traces of this loop and keep
refining the tuple of invariants $(I_i, I_{i+1}, \cdots I_n )$ until we find a
ranking function $\rf$ and the set of invariants that can prove the
termination of this loop. This is inductively done for all the loops till
$L_1$.

322

323\subsection{Theoretical Guarantees}

324Based on the assumption that the template of ranking functions incorporates
a finite set of possibilities and that the template for invariants is closed
under intersection and does not have an infinite descending chain (w.r.t the
partial order defined in Section~\ref{sec:theory}), we establish the soundness
and relative completeness of \toolname (as detailed in
Section~\ref{sec:efficiency}). Specifically, if there exist a valid ranking
function and an invariant from their respective templates for each loop that
can prove their termination, then \toolname will be able to prove their
termination. Conversely, in cases where no valid ranking function exists for a
loop w.r.t any invariants across all loops, \toolname terminates without
asserting the termination.

325% of the given program.

326% We used specific templates for ranking functions and invariants above,
but these templates can be generalized as long as the ranking function
template is finite, the invariant template is closed under intersection and
the partial order on the elements of the invariant template does not contain
an infinite descending chain. In Section~\ref{sec:theory}, we prove that under
certain assumptions, if there exist valid ranking functions and invariants
from their respective templates for each loop that can prove their
termination, then our algorithm will be able to prove their termination. We
also prove that if there is no ranking function for a loop that is valid
w.r.t. any sequence of invariants for all of the loops, our algorithm will
still terminate.

327

328% In the example above, we used specific templates for ranking functions
and invariants. These templates can be generalized to many other templates, as
long as they satisfy the following conditions:

329% \begin{enumerate}

330% \item The template of invariants ($\tempi$) is closed under intersection

331% \item The elements in $\tempi$ are partially ordered by the $\subseteq$
ordering and there is no infinite descending chain in $\tempi$.

332% \item The template for ranking functions ($\tempr$) is finite.

333% \item Given a valid invariant, $\invar$, and a program state $c$, it is
possible to sample a valid invariant, $\invar’$ such that $\invar’ \subseteq
\invar \setminus \\{c\\}$ iff such an invariant exists or determine that no
such invariant exists within finite time.

334% \item Given a relation, $t$, we can find a ranking function $f \in
\tempr$ that reduces and is bounded on $t$.

335% \item The validity-check of a ranking function w.r.t. a set of states and
a transition relation falls in a decidable theory.

336% \end{enumerate}

337% If the above conditions hold, we prove that the algorithm is sound and
complete in Section~\ref{sec:theory}.

##  3\. Preliminaries

#### Relations

For a pair of binary relations $R_{1}\subseteq A\times B$ and $R_{2}\subseteq
B\times C$, their _composition_ is the relation $R_{1}\circ
R_{2}=\\{(a,c)\>|\>\exists b\in B.\ (a,b)\in R_{1}\text{ and }(b,c)\in
R_{2}\\}\subseteq A\times C$. For a set $S\subseteq A$ and a binary relation
$R\subseteq A\times B$, $S\circ R=\\{b\in B\>|\>\exists a\in S.\ (a,b)\in
R\\}$ denotes the _image_ of $S$ under $R$. Finally, for a set $A$, the
_identity relation_ on $A$ is denoted as $\mathsf{id}_{A}=\\{(a,a)\>|\>a\in
A\\}$.

#### While Programs

To illustrate our synergistic synthesis approach, we will consider programs in
a simple while programming language whose BNF grammar is given below. In what
follows, $x$ is a program variable, $e$ a program expression and $\beta$ a
Boolean expression. The syntax of expressions is not given as it is not
important to the main ideas of this paper.

$\begin{array}[]{rcl}\mathsf{P}&::=&\texttt{skip}\ |\ x\leftarrow e\ |\
\mathsf{P}\>\text{;}\>\mathsf{P}\ |\ \texttt{if }\beta\texttt{ then
}\mathsf{P}\texttt{ else }\mathsf{P}\ |\ \texttt{while }\beta\texttt{ do
}\mathsf{P}\texttt{ od}\end{array}$

A _loop-free_ program code is one that does not have any while-loops. We will
typically use $\mathsf{P},\mathsf{P}_{1},\mathsf{P}_{2},\ldots$ to denote
programs, $\alpha,\alpha_{1},\ldots$ to denote loop-free programs, and
$\mathsf{L},\mathsf{L}_{1},\ldots$ to denote loops, i.e., programs of the form
$\texttt{while }\beta\texttt{ do }\mathsf{P}\text{ od}$.

Towards defining the semantics for a program $\mathsf{P}$, it is useful to
introduce the notion of a program state. A _program state_ $s$ of $\mathsf{P}$
assigns values to each variable of $\mathsf{P}$. The set of program states of
$\mathsf{P}$ will be denoted as $S_{\mathsf{P}}$. When the program
$\mathsf{P}$ is clear from the context, we will abuse notation and simply use
$S$ to denote all possible program states of $\mathsf{P}$, which is
represented by the invariant $\mathsf{I}_{\mathsf{true}}$. The semantics of a
program $\mathsf{P}$ denoted $\llbracket\mathsf{P}\rrbracket$, is a binary
relation on $S$ that captures how a program state is transformed when
$\mathsf{P}$ is executed. Assuming standard expressions and their semantics,
one can naturally define the semantics of loop-free programs. Loops present a
challenge. We will use _invariants_ to over-approximate their semantics. This
is also the reason why we will use relational semantics, as opposed to partial
functions.

##  4\. Annotated Programs

As explained in Sections LABEL:sec:nestedloops and 3, in our approach, we
approximate the reachable states and the semantics of loops using invariants.
So, it is useful to associate invariants with each loop in the program. The
set of invariants used to annotate loops will be from a template language. Let
us fix a collection $\mathcal{I}\subseteq 2^{S}$ of _invariants_ , where $S$
is the set of program states. For technical reasons that we will emphasize
later, we will assume that $\mathcal{I}$ is closed under intersection. That
is, for any $\mathsf{I}_{1},\mathsf{I}_{2}\in\mathcal{I}$,
$\mathsf{I}_{1}\cap\mathsf{I}_{2}\in\mathcal{I}$. Using the invariants in
$\mathcal{I}$, we define annotated programs as programs defined by the BNF
grammar below, where $\mathsf{I}$ is a member of $\mathcal{I}$.

$\begin{array}[]{rcl}\mathsf{A}&::=&\texttt{skip}\ |\ x\leftarrow e\ |\
\mathsf{A}\>\text{;}\>\mathsf{A}\ |\ \texttt{if }\beta\texttt{ then
}\mathsf{A}\texttt{ else }\mathsf{A}\ |\ \mathsf{I}\>@\>\texttt{while
}\beta\texttt{ do }\mathsf{A}\texttt{ od}\end{array}$

The main difference between (unannotated) programs and the above grammar is
that loops are annotated with an invariant as in the case
$\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do }\mathsf{A}\texttt{ od}$. We
will use $\mathsf{A},\mathsf{A}_{1},\ldots$ to denote annotated programs. For
an annotated program $\mathsf{A}$, its _underlying program_ can obtained by
removing the invariant annotations on the while-loops and we denote this as
$\mathcal{C}(\mathsf{A})$. This is defined in the Appendix A (Definition A.1).
For a (unannotated) program $\mathsf{P}$, the collection of all annotated
programs over $\mathsf{P}$ will be denoted by $\mathsf{A}(\mathsf{P})$, i.e.,
$\mathsf{A}(\mathsf{P})=\\{\mathsf{A}\>|\>\mathcal{C}(\mathsf{A})=\mathsf{P}\\}$.
We will use $\mathsf{A}_{\mathsf{L}}$ to denote an annotated subprogram of
$\mathsf{A}$ that corresponds to the loop $\mathsf{L}$ in $\mathsf{A}$.

In the following Sections, we show how to use the invariants associated with
each loop. Primarily, they have two use cases - (i) over-approximating the
transition relation of a loop (Section 4.1), (ii) over-approximating the set
of initial states for each loop (Section 4.2). Then we describe how to use
annotated programs to define the validity of ranking functions (Section 4.3).
We also define a partial order and meet operation over them (Section 4.4).
Using these definitions, we ensure that Syndicate refines the state in each
iteration and is complete even for arbitrarily nested loops.

###  4.1. Semantics of Annotated Programs

To define the approximate semantics of an annotated program $\mathsf{A}$ that
captures the terminating computations of $\mathsf{A}$, we assume a standard
semantics of program expressions and Boolean expressions which can be used to
define the semantics of loop-free programs in a natural way. We take
$\llbracket\alpha\rrbracket$ to be the transition semantics of a loop-free
program $\alpha$ and $\llbracket\beta\rrbracket\subseteq S$ to be the
semantics of a Boolean expression $\beta$. The semantics of an annotated
program $\mathsf{A}$ is defined inductively as follows.

$\displaystyle\llbracket\alpha\rrbracket$ $\displaystyle\triangleq\
\llbracket\alpha\rrbracket$ $\displaystyle\llbracket\texttt{if }\beta\texttt{
then }\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2}\rrbracket$
$\displaystyle\triangleq\
\mathsf{id}_{\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}_{1}\rrbracket\cup\mathsf{id}_{\llbracket\neg\beta\rrbracket}\circ\llbracket\mathsf{A}_{2}\rrbracket$
$\displaystyle\llbracket\mathsf{A}_{1}\>;\>\mathsf{A}_{2}\rrbracket$
$\displaystyle\triangleq\
\llbracket\mathsf{A}_{1}\rrbracket\circ\llbracket\mathsf{A}_{2}\rrbracket$
$\displaystyle\llbracket\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do
}\mathsf{A}_{1}\texttt{ od}\rrbracket$ $\displaystyle\triangleq\
\mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket)$

The difference between the semantics of an annotated program and that of a
regular (unannotated) program lies in the case of loops:
$\llbracket\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do
}\mathsf{A}_{1}\texttt{ od}\rrbracket$. We can over-approximate the semantics
of the loop body $\llbracket\mathsf{A}_{1}\rrbracket$ using the associated
invariant $\mathsf{I}$. The reachable states, $\mathcal{R}$, at the entry of
the while-loop, must satisfy the invariant. So,
$\mathcal{R}\subseteq\mathsf{I}$. The states that satisfy $\beta$ enter the
loop, while the states that do not satisfy $\beta$ exit. So, the transition
relation is over-approximated by
$\mathsf{I}\times(\mathsf{I}\cap\llbracket\neg\beta\rrbracket)$.

###  4.2. Correctness of Annotated Programs

Annotations of invariants in an annotated program $\mathsf{A}$ are expected to
be inductive loop invariants for the while-loops they decorate. Without such
an assumption, the semantics defined in the previous paragraph will not
accurately describe the terminating computations of the program. Recall that
an _inductive invariant_ $\mathsf{I}$ is a set of program states that
satisfies the following two properties: (Initiation) $\mathsf{I}$ contains all
program states you could enter the loop in; (Consecution) If you run the loop
body from a state in $\mathsf{I}$, you end up in a state that also belongs to
$\mathsf{I}$. Based on this, we can define what it means for all the
annotations in a program to be correct. Notice that correctness needs to be
defined w.r.t a set of initial states. Let $Init\subseteq S$ be a set of
initial program states and let $\mathsf{A}$ be an annotated program.
$\mathsf{A}$ is said to be _correct_ with respect to initial states $Init$ if
the annotations in $\mathsf{A}$ are inductive invariants. This can be
inductively defined based on the structure of $\mathsf{A}$.

$\displaystyle Init\models\alpha$ $\displaystyle\triangleq\ \mathsf{true}$
$\displaystyle Init\models\texttt{if }\beta\texttt{ then
}\mathsf{A}_{1}\texttt{ else }\mathsf{A}_{2}$ $\displaystyle\triangleq\
(Init\cap\llbracket\beta\rrbracket\models\mathsf{A}_{1})\wedge(Init\cap\llbracket\neg\beta\rrbracket\models\mathsf{A}_{2})$
$\displaystyle Init\models\mathsf{A}_{1}\>;\>\mathsf{A}_{2}$
$\displaystyle\triangleq\
(Init\models\mathsf{A}_{1})\wedge(Init\circ\llbracket\mathsf{A}_{1}\rrbracket\models\mathsf{A}_{2})$
$\displaystyle Init\models\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do
}\mathsf{A}_{1}\texttt{ od}$ $\displaystyle\triangleq\
(Init\subseteq\mathsf{I})\wedge((\mathsf{I}\cap\llbracket\beta\rrbracket)\circ\llbracket\mathsf{A}_{1}\rrbracket\subseteq\mathsf{I}\times\mathsf{I})\wedge(Init\cap\llbracket\beta\rrbracket\models\mathsf{A}_{1})$

Note that in the above definition, given an initial set for the annotated
program $\mathsf{A}_{\mathsf{L}}$, we use its constituent invariants to
compute the initial set for the annotated subprograms of
$\mathsf{A}_{\mathsf{L}}$. The individual initial sets are consequently used
for defining the correctness of the annotated programs. In the case of a loop,
where $\mathsf{A}_{\mathsf{L}}\equiv\mathsf{I}\>@\>\texttt{while
}\beta\texttt{ do }\mathsf{A}_{1}\texttt{ od}$, the correctness condition also
checks the correctness of the invariant $\mathsf{I}$.

###  4.3. Correctness of Ranking Functions using Annotated Programs

A ranking function is a real-valued function $f$ on the program states that is
bounded from below and decreases by a minimum amount in every iteration of the
loop. For such a ranking function $f$ to be a valid witness for termination,
$f$ is only required to have these properties on the reachable states (or an
over-approximation of the reachable states) of the program rather than all the
program states. Given these observations, we define when a ranking function
proves the termination of an annotated while-loop, given an initial set of
states.

###### Definition 4.0 (Correctness of a Ranking Function).

Let $Init\subseteq S$ be a set of initial program states and
$f:S\to\mathbb{R}$ be a candidate ranking function. We say that $f$
_establishes_ the termination of annotated program
$\mathsf{A}_{\mathsf{L}}=\mathsf{I}\>@\>\texttt{while }\beta\texttt{ do
}\mathsf{A}\texttt{ od}$ from initial states $Init$, i.e.,
$Init\models\mathsf{A}_{\mathsf{L}},f$ if

  * •

The annotations of $\mathsf{A}_{\mathsf{L}}$ are correct with respect to
$Init$, i.e., $Init\models\mathsf{A}_{\mathsf{L}}$, and

  * •

For all
$(s,s^{\prime})\in\mathsf{id}_{\mathsf{I}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}\rrbracket$,
$f(s)\geq 0$ and $f(s)-f(s^{\prime})\geq 1$

Note that in Definition 4.1, we require that the ranking function $f$ be
positive and decrease by $1$ in each loop iteration. These may appear to be
strong requirements as typically, ranking functions are only required to be
bounded above some value (say $\theta$) and decrease by some minimum amount
(say $\delta$). However, if such a more general type of ranking function $g$
exists then the specific one of the type given in Definition 4.1 also exists:
just take $f(s)$ to be $(g(s)-\theta)/\delta$.

###  4.4. Meet-semilattice on Annotated programs

We introduce a partial order ($\preceq$) and a meet operation ($\wedge$) for
the set of annotated programs ($\mathsf{A}$), which are crucial to
understanding our algorithm. Let $\mathsf{A}$ be an annotated program such
that $\mathcal{C}(\mathsf{A})=\mathsf{P}$. For annotated programs
$\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P})$ (i.e.,
$\mathcal{C}(\mathsf{A}_{1})=\mathcal{C}(\mathsf{A}_{2})=\mathsf{P}$), we say
$\mathsf{A}_{2}\preceq\mathsf{A}_{1}$ if for each loop in $\mathsf{P}$, the
invariant annotating this loop in $\mathsf{A}_{2}$ is contained in the
corresponding invariant in $\mathsf{A}_{1}$; the formal definition is deferred
to Appendix A. If $\mathsf{A}_{2}\preceq\mathsf{A}_{1}$ and
$\mathsf{A}_{2}\neq\mathsf{A}_{1}$ then we say
$\mathsf{A}_{2}\prec\mathsf{A}_{1}$. Next,
$\mathsf{A}_{1}\wedge\mathsf{A}_{2}$ denotes the annotated program where each
loop is annotated by the intersection of the invariants annotating the loop in
$\mathsf{A}_{1}$ and $\mathsf{A}_{2}$.

In Appendix B, we show that if there are two annotated programs
$\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P})$ such that they are
valid w.r.t the initial set, i.e., $Init\models\mathsf{A}_{1}$ and
$Init\models\mathsf{A}_{2}$, then the meet of $\mathsf{A}_{1}$ and
$\mathsf{A}_{2}$ is also valid w.r.t the initial set, i.e.,
$Init\models\mathsf{A}_{1}\wedge\mathsf{A}_{2}$. Further, if $\mathsf{P}$ is a
loop program, if $\mathsf{A}_{1}$ and a ranking function $f$ are valid w.r.t
to the initial set, i.e. $Init\models\mathsf{A}_{1},f$, and $\mathsf{A}_{2}$
is a valid annotated program w.r.t $Init$ and
$\mathsf{A}_{2}\preceq\mathsf{A}_{1}$, then the pair $\mathsf{A}_{2},f$ is
also valid w.r.t $Init$. This can formally be presented as:

###### Proposition 4.0.

Let $\mathsf{A}_{1},\mathsf{A}_{2}\in\mathsf{A}(\mathsf{P})$ be two annotated
programs.

  1. (1)

If $Init\models\mathsf{A}_{2}$ and $Init\models\mathsf{A}_{1}$, then
$Init\models\mathsf{A}_{1}\wedge\mathsf{A}_{2}$.

  2. (2)

If $Init\models\mathsf{A}_{1},f$, $Init\models\mathsf{A}_{2}$, and
$\mathsf{A}_{2}\preceq\mathsf{A}_{1}$, then $Init\models\mathsf{A}_{2},f$.

##  5\. Syndicate Framework

Before describing our algorithm, we fix templates for the set of possible
invariants $\mathcal{I}$ and possible ranking functions $\mathcal{F}$. The
algorithm can be instantiated with any templates (which can be different for
each loop in the program), provided they satisfy the computability assumptions
described in Theorem 5.3. We assume that the set of all possible program
states ($\mathsf{I}_{\mathsf{true}}$) is in $\mathcal{I}$ and that
$\mathcal{I}$ is closed under intersection, i.e., if
$\mathsf{I}_{1},\mathsf{I}_{2}\in\mathcal{I}$ then
$\mathsf{I}_{1}\cap\mathsf{I}_{2}\in\mathcal{I}$. Let us also fix a program
$\mathsf{P}$ and a set of initial states $Init$. The goal is to synthesize
ranking functions from $\mathcal{F}$ and invariants from $\mathcal{I}$ that
demonstrate that every loop inside $\mathsf{P}$ terminates. In the following
section, we describe an algorithm that is both _sound_ and _complete_ —
ranking functions and invariants identified constitute a correct proof of
termination, and if there is a proof of termination using invariants in
$\mathcal{I}$ and ranking functions from $\mathcal{F}$ then the algorithm does
succeed. We first establish such a result under assumptions about the sets
$\mathcal{I}$ and $\mathcal{F}$ and some computability assumptions about sub-
procedures of our main algorithm. We then present algorithms for the sub-
procedures that satisfy the computability assumptions needed for the soundness
and completeness result.

###  5.1. Algorithm State

Consider a situation where our algorithm is trying to prove the termination of
a loop $\mathsf{L}=\texttt{while }\beta\texttt{ do }\mathsf{P}_{1}\texttt{
od}$ inside program $\mathsf{P}$. Syndicate maintains an algorithm state which
is used to guess a candidate ranking function, and also check its correctness.
It then iteratively refines its state until convergence. The algorithm state
has two components: (1) an annotated program
$\mathsf{A}\in\mathsf{A}(\mathsf{P})$ such that $Init\models\mathsf{A}$; this
can be easily initialized by labeling each loop in $\mathsf{P}$ with $S$, the
set of all program states, (2) a finite set $\mathsf{t}\subseteq S\times S$
such that for any correct annotation $\mathsf{A}^{\prime}$ of $\mathsf{P}$,
$\mathsf{t}\subseteq\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket$,
where $\mathsf{I}^{\prime}$ is the annotation of $\mathsf{L}$ in
$\mathsf{A}^{\prime}$. Since the pairs in $t$ are in the semantics of the loop
body $\mathsf{P}_{1}$, it can be used to guess a candidate ranking function
from the set
$\Pi(\mathsf{t},\mathcal{F})\triangleq\\{f\in\mathcal{F}\>|\>\forall(s,s^{\prime})\in\mathsf{t},f(s)\geq
0\wedge f(s)-f(s^{\prime})\geq 1\\}$, that contains all the functions that
reduce and are bounded on the pairs in $t$. Next, the annotated program can be
used to check the validity of the guessed candidate ranking functions.

#### Refinement of the Algorithm State

$\mathsf{A}$$\mathsf{A}^{\prime}$$\mathsf{A}^{*}$ Figure 2. Assume that
$\mathsf{A}^{*}$ can prove the validity of $f$. Since
$\mathsf{A}^{\prime}\preceq\mathsf{A}$, $\mathsf{A}$ can be refined to
$\mathsf{A}^{\prime}$, which can also prove the validity of $f$.

Checking the correctness of $f$ may lead to at least one of the following
cases. (1) The identification of additional pairs of states
$(s_{i},s^{\prime}_{i})\notin t$ over which every valid ranking function must
decrease. We add these newly discovered pairs to the algorithm state, i.e.,
$t^{\prime}\leftarrow t\cup\\{(s_{i},s^{\prime}_{i})\\}$. As a consequence,
$\Pi(\mathsf{t}^{\prime},\mathcal{F})\subset\Pi(\mathsf{t},\mathcal{F})$. (2)
The refinement of the annotated program to $\mathsf{A}^{\prime}$ such that
$\mathsf{A}^{\prime}\prec\mathsf{A}$. Thus, the algorithm progresses either by
eliminating additional potential ranking functions or constructing a more
precise model for the semantics of the program by a progressive refinement of
the annotations of $\mathsf{P}$. An important observation at this point is
that in our algorithm, we always refine the annotations of the $\mathsf{P}$,
i.e. the new annotation $\mathsf{A}^{\prime}$ is always $\preceq\mathsf{A}$.
In Lemma 5.1, we prove that if there exists an annotated program
$\mathsf{A}^{*}$ which proves the validity of a ranking function $f$, then
there also exists an annotated program $\mathsf{A}^{\prime}\preceq\mathsf{A}$,
which can prove $f$ valid (Fig. 2). This means that by refining the program’s
annotations, we narrow down the space of all possible annotations without
eliminating the possibility of verifying the validity of any correct ranking
function.

###### Lemma 5.0.

Let $\mathsf{A},\mathsf{A}^{*}\in\mathsf{A}(\mathsf{P})$ and $f$ be a ranking
function. If $Init\models\mathsf{A}$ and $Init\models\mathsf{A}^{*},f$ then
$\exists\mathsf{A}^{\prime}\preceq\mathsf{A}$ and
$Init\models\mathsf{A}^{\prime},f$.

###### Proof.

Let $\mathsf{A}^{\prime}=\mathsf{A}\wedge\mathsf{A}^{*}$. Clearly,
$\mathsf{A}^{\prime}\preceq\mathsf{A}$. It follows from Proposition 4.2 that
$Init\models\mathsf{A}^{\prime},f$. ∎

###  5.2. Detailed Algorithm

Syndicate (Algorithm 1) iteratively generates a candidate ranking function and
then uses it to refine the algorithm state if the candidate ranking function
is not valid. The function get_candidate (line 5) returns a ranking function
from the set $\Pi(\mathsf{t},\mathcal{F})$ if one exists and returns
$\mathsf{false}$ if $\Pi(\mathsf{t},\mathcal{F})$ is empty. The function check
(line 10) returns $\mathsf{true}$ if $Init\models\mathsf{A},f$ and
$\mathsf{false}$ otherwise. We assume that if check fails, get_cex produces a
_counter-example_ (line 13). The counter-example is a pair of states
$(p,p^{\prime})$ such that (a)
$(p,p^{\prime})\in\llbracket\mathsf{A}[\mathsf{P}_{1}]\rrbracket$, (b)
$p\in\mathsf{I}\cap\llbracket\beta\rrbracket$, where $\mathsf{I}$ is the
invariant labeling $\mathsf{L}$ in $\mathsf{A}$, and (c) either $f(p)<0$ or
$f(p)-f(p^{\prime})<1$.

Algorithm 1 Syndicate

Inputs: $\mathsf{t}$ \- Set of traces, $\mathsf{A}$ \- Program annotated with
the invariants (initialized with $\mathsf{I}_{\mathsf{true}}$)
Output: $\mathsf{true}$ if termination is proved, $\mathsf{false}$ otherwise

1:procedure find_ranking($\mathsf{t},\mathsf{A}$)

2: $\texttt{is\\_refined}\leftarrow\mathsf{false}$

3: while $\mathsf{true}$ do

4: if $\neg\texttt{is\\_refined}$ then

5:
$\texttt{gen},f\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_candidate}}}}(\mathsf{t})$

6: if $\neg\texttt{gen}$ then

7: return $\mathsf{false}$

8: end if

9: end if

10: if
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{check}}}}(f,\mathsf{A})$
then

11: return $\mathsf{true}$

12: end if

13:
$(p,p^{\prime})\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_cex}}}}(f,\mathsf{A})$

14:
$\texttt{is\\_refined},\;\mathsf{A},t\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),t)$

15: if $\neg\texttt{is\\_refined}$ then

16: $\mathsf{t}\leftarrow\mathsf{t}\cup\\{(p,p^{\prime})\\}$

17: end if

18: end while

19:end procedure

If $f$ is not a valid ranking function for $\mathsf{L}$ then the counter-
example $(p,p^{\prime})$ is used to refine the program state (line 14). The
counter-example can be eliminated in one of two ways: (1) The invariants in
$\mathsf{A}$ are refined so that $p$ is not an entry state of loop
$\mathsf{L}$ or $(p,p^{\prime})$ is not in the semantics of the body
$\mathsf{P}_{1}$, or (2) A new ranking function is synthesized that behaves
correctly on the pair $(p,p^{\prime})$. The subroutine refine (line 14) tries
to eliminate $(p,p^{\prime})$ by refining the invariants in $\mathsf{A}$. The
crucial property we require of refine is as follows.

  1. (1)

If
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t})$
returns $(\mathsf{true},\mathsf{A}^{\prime},t^{\prime})$ then it must be the
case $\mathsf{A}^{\prime}\prec\mathsf{A}$ and
$Init\models\mathsf{A}^{\prime}$.

  2. (2)

If
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t})$
returns $(\mathsf{false},\mathsf{A}^{\prime},t^{\prime})$ then
$\mathsf{A}^{\prime}=\mathsf{A}$ and for every correct
$\mathsf{A}^{\prime\prime}$ (i.e. $Init\models\mathsf{A}^{\prime\prime}$) with
$\mathsf{A}^{\prime\prime}\prec\mathsf{A}$,
$(p,p^{\prime})\in\mathsf{id}_{\mathsf{I}^{\prime\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime\prime}[\mathsf{P}_{1}]\rrbracket$
where $\mathsf{I}^{\prime\prime}$ is the invariant labelling $\mathsf{L}$ in
$\mathsf{A}^{\prime\prime}$. In other words, $(p,p^{\prime})$ is in the
semantics of the body of the loop $\mathsf{L}$ in every refinement of
$\mathsf{A}$.

In both of the above cases, $t\subseteq
t^{\prime}\subseteq\llbracket\mathsf{P}_{1}\rrbracket$ and
$\mathsf{dom}(t^{\prime})\subseteq\mathcal{R}$. Note that if refine is unable
to refine (returns $\mathsf{false}$), then by the definition of refine, for
every $\mathsf{A}^{\prime\prime}\prec\mathsf{A}$, $(p,p^{\prime})$ is in the
semantics of the loop $\mathsf{L}$ captured by $\mathsf{A}^{\prime\prime}$.
The following lemma lifts this to all possible valid
$\mathsf{A}^{\prime\prime}$ and proves that if refine returns
$\mathsf{false}$, it means that $(p,p^{\prime})$ is in the semantics of the
loop $\mathsf{L}$ captured by all valid annotated programs (not limited to
$\prec\mathsf{A}$). So, we add $(p,p^{\prime})$ to $\mathsf{t}$ to get a new
set $\mathsf{t}_{\mathsf{new}}$. Note that $\mathsf{t}_{\mathsf{new}}$
continues to satisfy the property that we required of $\mathsf{t}$.

###### Lemma 5.0.

Suppose
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{refine}}}}(\mathsf{A},(p,p^{\prime}),\mathsf{t})$
returns $(\mathsf{false},\mathsf{A},t^{\prime})$. Consider any annotated
program $\mathsf{A}^{\prime}\in\mathsf{A}(\mathsf{P})$ such that
$Init\models\mathsf{A}^{\prime}$. Let $\mathsf{I}^{\prime}$ be the annotation
of $\mathsf{L}$ in $\mathsf{A}^{\prime}$. Then
$(p,p^{\prime})\in\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket$.

###### Proof.

Suppose the claim is not true, i.e., for some correct annotated program
$\mathsf{A}^{\prime}$,
$(p,p^{\prime})\not\in\mathsf{id}_{\mathsf{I}^{\prime}\cap\llbracket\beta\rrbracket}\circ\llbracket\mathsf{A}^{\prime}[\mathsf{P}_{1}]\rrbracket$.
Consider the program $\mathsf{A}\wedge\mathsf{A}^{\prime}\prec\mathsf{A}$. By
Lemma 5.1, $\mathsf{A}\wedge\mathsf{A}^{\prime}$ is correct and
$(p,p^{\prime})$ is not valid pair for the semantics of the loop body
$\mathsf{P}_{1}$. In such a case refine must return $\mathsf{true}$ giving us
the desired contradiction. ∎

By processing counter-example $(p,p^{\prime})$, our algorithm always makes
progress. There are two cases to consider. If refine returns $\mathsf{true}$
then we have a new correct annotated program $\mathsf{A}^{\prime}$ that
refines $\mathsf{A}$. On the other hand, if refine returns $\mathsf{false}$
then we have new set $\mathsf{t}_{\mathsf{new}}$ with the property that
$\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F})\subsetneq\Pi(\mathsf{t},\mathcal{F})$.
This is because
$f\in\Pi(\mathsf{t},\mathcal{F})\setminus\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F})$
since $f$ is not a valid ranking function for the pair $(p,p^{\prime})$. Thus,
in this case $\Pi(\mathsf{t}_{\mathsf{new}},\mathcal{F})$ has become smaller.

###  5.3. Soundess, Completeness, and Efficiency of Syndicate

Algorithm 1 can be shown to be sound and complete for proving the termination
of loop $\mathsf{L}$ of $\mathsf{P}$. In this context, soundness means that if
our algorithm succeeds and returns a ranking function $f$ from $\mathcal{F}$,
then there exists an invariant in $\mathcal{I}$ that can prove that $f$ is a
valid ranking function for $\mathsf{L}$. Conversely, completeness means that
if there is a function $f\in\mathcal{F}$ and $\mathsf{I}\in\mathcal{I}$ such
that $f$ can be proved valid using $\mathsf{I}$, then Algorithm 1 will prove
termination.

###### Theorem 5.3.

Suppose there exist complete procedures for the functions get_candidate,
check, get_cex, and refine that satisfy the properties defined above. Further,
suppose the set $\mathcal{F}$ is finite, and $\mathcal{I}$ is closed under
intersection and has no infinite descending chains (w.r.t the subset
relation). Then Algorithm 1 is a sound and complete method to prove the
termination of loop $\mathsf{L}$ of $\mathsf{P}$.

###### Proof Sketch.

The soundness of the algorithm follows from the semantics of get_candidate and
check. Suppose there is a ranking function $f^{*}$ and an annotated program
$\mathsf{A}^{*}$ such that $\mathsf{A}^{*}$ is a correct annotation of
$\mathsf{P}$ and $f^{*}$ is a valid ranking function that proves the
termination of $\mathsf{L}$. Let $(\mathsf{A},\mathsf{t})$ be the state of the
algorithm at any point. Observe that because of the property that the
algorithm maintains of $\mathsf{t}$, we have
$f^{*}\in\Pi(\mathsf{t},\mathcal{F})$. By Lemma 5.1 there is a correct
annotated program
$\mathsf{A}^{\prime}(=\mathsf{A}\wedge\mathsf{A}^{*})\preceq\mathsf{A}$ such
that $f^{*}$ proves the termination of $\mathsf{L}$ in $\mathsf{A}^{\prime}$.
Finally, the assumptions on $\mathcal{I}$ and $\mathcal{F}$ mean that
$\Pi(\mathsf{t},\mathcal{F})$ and
$\mathsf{A}\downarrow=\\{\mathsf{A}^{\prime}\>|\>\mathsf{A}^{\prime}\preceq\mathsf{A}\\}$
are both finite sets and hence there can only be finitely many steps of
refinement. Thus Algorithm 1 will terminate with the right answer. ∎

#### Efficiency

Consider a meet semilattice ($\mathcal{L}_{\mathcal{F}},\preceq,\wedge)$
induced by $\mathcal{F}$ where each element is a set of ranking functions from
$\mathcal{F}$ and $\preceq,\wedge$ are defined by the set operations
$\subseteq,\cap$. In each refinement step, we either (1) add a pair of states
to $\mathsf{t}$ creating $\mathsf{t}_{new}$, which in turn decreases the size
of the set of ranking functions $\Pi$ determined by the algorithm’s state, as
$\Pi(\mathsf{t}_{new},\mathcal{F})\subset\Pi(\mathsf{t},\mathcal{F})$. The
number of times this refinement can be performed is bounded by the depth of
the semilattice $\mathcal{L}_{\mathcal{F}}$, or (2) we refine the current
annotation $\mathsf{A}$ to $\mathsf{A}^{\prime}$, where
$\mathsf{A}^{\prime}\prec\mathsf{A}$. This is bounded by the depth of the meet
semilattice for the annotated programs $\mathcal{L}_{\mathsf{A}}$. This bounds
the number of iterations of our algorithm to
$\mathsf{depth}(\mathcal{L}_{\mathcal{F}})+\mathsf{depth}(\mathcal{L}_{\mathsf{A}})$.
This worst-case bound is much better than the unguided search for invariants
and ranking functions. A naive termination algorithm that searches for
invariants and ranking functions independently would realize a worst-case
bound of $|\mathcal{L}_{\mathcal{F}}|\ \times\ |\mathcal{L}_{\mathsf{A}}|$,
where $|\cdot|$ represents the number of elements in the lattice. Even a
strategy that ensures refinement at each step of the algorithm, and hence a
downward movement in their respective lattice, would have a worst-case bound
of
$\mathsf{depth}(\mathcal{L}_{\mathcal{F}})\times\mathsf{depth}(\mathcal{L}_{\mathsf{A}})$.
Thus, we argue that Syndicate’s synergistic synthesis for invariants and
ranking functions has significant merit. In Section 7, we show that Syndicate
is better than the state-of-the-art termination analysis tools in terms of
runtime analysis for non-trivial programs.

###  5.4. Detailed Subprocedures

Algorithm 2 Algorithm for Refine State

Inputs: Annotated program ($\mathsf{A}$), counter-example ($(p,p^{\prime}$),
reachable state pairs ($t$)
Output: $\mathsf{true}$ or $\mathsf{false}$, refined annotated program
($\mathsf{A}^{\prime}$), additional reachable states pairs ($t$)

1:procedure $\mathsf{refine}$($\mathsf{A},(p,p^{\prime}),t$)

2: $\mathsf{inv_{c}}$ = []

3:
$\mathsf{A}^{\prime},\text{gen}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_inv}}}}(t,(p,p^{\prime}),\mathsf{inv_{c}})$

4: while gen do

5: if
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{check\\_inv}}}}(\mathsf{A}^{\prime})$
then

6: return $\mathsf{true}$, $\mathsf{A}\wedge\mathsf{A}^{\prime}$, $t$

7: end if

8:
$(c,c^{\prime}),\mathsf{for\\_pre}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_cex\\_inv}}}}(\mathsf{A}^{\prime})$

9: if $\mathsf{for\\_pre}$ then

10: $t\leftarrow t\cup\\{(c,c^{\prime})\\}$

11: else

12: $\mathsf{inv_{c}}\leftarrow\mathsf{inv_{c}}\cup\\{(c,c^{\prime})\\}$

13: end if

14:
$\mathsf{A}^{\prime},\text{gen}\leftarrow\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_inv}}}}(t,(p,p^{\prime}),\mathsf{inv_{c}})$

15: end while

16: return $\mathsf{false}$, $\mathsf{A}$, $t$

17:end procedure

We describe procedures for get_candidate, check, get_cex, and refine that
satisfy the assumptions needed for soundness and completeness of Algorithm 1.
For these procedures, we use SMT queries to generate and check the soundness
of ranking functions for a given loop. We can define $\mathcal{F}$ as a finite
template for ranking functions. For the function get_candidate, given $t$, we
can generate an SMT query encoding a symbolic ranking function in
$\mathcal{F}$ that satisfies the reducing and bounded conditions for all of
the pairs of states in $t$. Finding a satisfying assignment to this query is
equivalent to finding a candidate ranking function and if there is no
satisfying assignment, then there is no ranking function in $\mathcal{F}$ that
is valid for the under-approximation, $t$, and, therefore, there is no ranking
function in $\mathcal{F}$ that is valid for the loop. This follows the
semantics of get_candidate described in Section 5.2. For this function to be
decidable, one must be able to describe the set of all ranking functions in
$\mathcal{F}$ and express the bounded and reducing conditions on these ranking
functions in a decidable SMT theory. Some examples of templates that lead to
the SMT queries being decidable are the set of linear functions over the
program variables, the set of polynomial functions over the program variables
using real-valued coefficients, and the set of lexicographic functions where
each component is a polynomial function using real-valued coefficients.

We can also use an SMT query for a function that implements the semantics of
both check and get_cex. check checks the validity of $f$ given $\mathsf{A}$.
First, we define variables representing the state at the start of one
iteration of the loop, $(x_{1},\cdots,x_{j})$, and add the condition
$(x_{1},\cdots,x_{j})\in\mathsf{I}$ where $\mathsf{I}$ is the invariant of the
loop we are analyzing, retrieved from $\mathsf{A}$. Then, we encode the over-
approximation of the loop body defined by $\mathsf{A}$ into the SMT query. For
each loop in the body of the outer loop, we define new variables,
$(x_{i,1},\cdots,x_{i,j})$ to represent the states at the exit of each inner
loop, adding the condition
$(x_{i,1},\cdots,x_{i,j})\in\mathsf{I}_{i}\cap\llbracket\neg\beta_{i}\rrbracket$,
where $\mathsf{I}_{i}$ and $\beta_{i}$ are the invariant and loop guard of the
inner loop from $\mathsf{A}$. We define variables representing the state at
the end of the iteration, $(x^{\prime}_{1},\cdots,x^{\prime}_{j})$, and set
these variables equal to the output state of $\llbracket\mathsf{A}\rrbracket$
when the input state is $(x_{1},\cdots,x_{j})$. Checking the validity of $f$
using $\mathsf{A}$ is reduced to determining the satisfiability of the
formula:
$(f(x_{1},\cdots,x_{j})-f(x^{\prime}_{1},\cdots,x^{\prime}_{j})<1)\vee(f(x_{1},\cdots,x_{j})<0)$.
If this formula is unsatisfiable, then we have proven the validity of $f$
because we have established that $f$ is bounded and reducing on the possible
state of the loop. If this formula is unsatisfiable, we return
$\mathsf{true}$. Otherwise, we return $\mathsf{false}$. In Algorithm 1,
get_cex is only called when check returns $\mathsf{false}$. In this case, from
the SMT query in check, we have a satisfying assignment to
$(x_{1},\cdots,x_{j})$ and $(x^{\prime}_{1},\cdots,x^{\prime}j)$. The counter-
example, $(p,p^{\prime})$, returned by
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_cex}}}}(f,\mathsf{A})$
is $((x_{1},\cdots,x_{j}),(x^{\prime}_{1},\cdots,x^{\prime}_{j}))$. For this
algorithm to be decidable, the SMT encoding of the program has to fit into a
decidable SMT theory.

We now describe an algorithm that implements the semantics of the refine
function and follows the properties defined in Section 5.2. Since we defined
check to define symbolic states,$(x_{i,1},\cdots,x_{i,j})$, at the end of each
inner loop, instead of only storing $(p,p^{\prime})$, check can store
$(p_{1},\cdots,p_{m})$, where $p_{1}=p$, $p_{m}=p^{\prime}$ and
$p_{i}=(x_{i,1},\cdots,x_{i,j})$ for all $i\in[1,m]$. This sequence of states
will be used to define refine, shown in Algorithm 2.

First, we define how the refine function works when considering a single loop,
and then extend it to multiple loops, nested or sequential. When refining the
invariant for a non-nested loop given a candidate ranking function, $f$, and a
counter-example, $(p,p^{\prime})$, for $f$ to be a valid ranking function, $p$
has to not be a reachable state the beginning of one iteration of the outer
loop. In our algorithm state, for a non-nested loop, we have an annotated
program with one invariant, $\mathsf{I}$. First we try to refine $\mathsf{I}$
to $\mathsf{I}^{\prime}$ s.t.
$\mathsf{I}^{\prime}\subseteq\mathsf{I}\setminus\\{p\\}$. For this, we first
try to find an invariant, $\mathsf{I}^{\prime\prime}$, that is a valid
invariant and excludes the state $p$ and if this is possible, we return
$\mathsf{I}\cap\mathsf{I}^{\prime\prime}$. Note that
$\mathsf{I}\cap\mathsf{I}^{\prime\prime}\in\mathcal{I}$ because $\mathcal{I}$
is closed under intersection and
$\mathsf{I}\cap\mathsf{I}^{\prime\prime}\subseteq\mathsf{I}\setminus\\{p\\}$.
To find $\mathsf{I}^{\prime\prime}$, we iteratively generate possible
invariants and then check their validity until either we have found a valid
invariant that excludes $p$ or proved that no such invariant exists. We show
this procedure in Algorithm 2. In lines 3 and 14, we generate new possible
invariants. In line 5, we check the validity of the invariant. In lines 9-13,
based on the output of the validity check we update the information used to
generate new invariants.

To generate a possible invariant that excludes $p$, we want to generate a set
from $\mathcal{I}$ that excludes $p$ and includes the states we know are
reachable, $\mathsf{dom}(t)$. After we generate a possible invariant,
$\mathsf{I}_{1}$, we check whether it includes $Init$ and is inductive. If
$\mathsf{I}_{1}$ does not include $Init$, we obtain a state, $c\in Init$, s.t.
$c\notin\mathsf{I}_{1}$. When we generate the next possible invariant,
$\mathsf{I}_{2}$, we add the condition $c\in\mathsf{I}^{\prime\prime}$. This
condition is added by adding $(c,c^{\prime})$ to $t$. If, on the other hand,
$\mathsf{I}^{\prime}$ is not inductive, we obtain a counter-example,
$(c,c^{\prime})$ s.t. $c\in\mathsf{I}_{1}\wedge
c^{\prime}\notin\mathsf{I}_{1}$. In this case, to ensure we generate a
different possible invariant, $\mathsf{I}_{2}$, we add the condition
$c\in\mathsf{I}_{2}\implies c^{\prime}\in\mathsf{I}_{2}$. Note that the
conditions we add in each iteration of generating possible invariants are
$\mathsf{true}$ for all valid invariants of a loop.

We use $inv_{c}$ to represent the set of pairs of states we obtained as
counter-examples in previous iterations of checking the validity of possible
invariants. $inv_{c}$ is initialized to $\\{\\}$. We use the following SMT
queries to find a candidate for $\mathsf{I}^{\prime\prime}$ (get_inv), and
check its correctness (check_inv) respectively.

(3)
$\Big{(}p\notin\mathsf{I}^{\prime\prime}\Big{)}\wedge\Big{(}\bigwedge_{(s,s^{\prime})\in
t}s\in\mathsf{I}^{\prime\prime}\Big{)}\wedge\Big{(}\bigwedge_{(s,s^{\prime})\in
inv_{c}}s\in\mathsf{I}^{\prime\prime}\implies
s^{\prime}\in\mathsf{I}^{\prime\prime}\Big{)}$ (4) $\Big{(}s\in Init\wedge
s\notin\mathsf{I}^{\prime\prime}\Big{)}\vee\Big{(}s\in\mathsf{I}^{\prime\prime}\wedge\llbracket\mathsf{P}\rrbracket
s\notin I^{\prime\prime}\Big{)}$

If the SMT query checking the validity of $\mathsf{I}^{\prime\prime}$ is
satisfiable, get_cex_inv either returns a state $(c,c^{\prime})$, s.t. $c\in
Init\wedge(c,c^{\prime})\not\in\mathsf{I}^{\prime\prime}$ or returns a pair of
states $(c,c^{\prime})$ where $c\in\mathsf{I}^{\prime\prime}\wedge
c^{\prime}\notin I^{\prime\prime}$. In the former case, we add this state to
$t$ (line 10). In the latter case, we add this state to $inv_{c}$ (line 12).
With updated $t$ and $inv_{c}$, we repeat the process of generating and
checking a new possible invariant.

###  5.5. Multiple Loops

In the case of multiple loops, we need to find
$\mathsf{A}^{\prime}\prec\mathsf{A}$, where $\mathsf{A}$ is the annotated loop
program in our algorithm state. As discussed earlier, in this instantiation of
our framework, check will return $(p_{1},\cdots,p_{m})$ instead of only
$(p,p^{\prime})$. So, we have counter-examples, $p_{i}$, for each invariant,
$\mathsf{I}_{i}$, in the program. For each invariant, we maintain the set,
$t_{i}$ and $inv_{c_{i}}$. $t_{i}$ is initialized to the set of states after
the loop associated with $\mathsf{I}_{i}$ obtained for the initial program
execution traces and $inv_{c_{i}}$ is initialized to an empty set. We use an
SMT query to generate a candidate invariants, $\mathsf{I}^{\prime}_{i}$ for
all of the loops such that at least one of the loops in $\mathsf{A}$ that
excludes the counter-example, $p_{i}$ associated with $\mathsf{I}_{i}$.
Formally, we find a satisfying assignment to the constants in
$\mathsf{I}^{\prime}_{i}$ such that

(5) $\bigvee_{i}\Big{(}\neg
p_{i}\in\mathsf{I}_{i}\wedge\bigwedge_{(s,s^{\prime})\in
t_{i}}s\in\mathsf{I}_{i}\wedge(\bigwedge_{(s,s^{\prime})\in
inv_{c_{i}}}s\in\mathsf{I}_{i}\implies s^{\prime}\in\mathsf{I}_{i})\Big{)}$

Once we find candidate invariants for all of the loops such that for at least
one of the loops, $\mathsf{I}^{\prime}_{i}$ excludes $p_{i}$, we check the
validity of the candidate invariants. This validity check is done the same way
as in the single loop case, and the counter-examples are either added to
$t_{i}$ or $inv_{c_{i}}$ accordingly. We repeatedly generate candidates to
refine at least one of the invariants until one is found or there does not
exist any valid invariant for any of the loops that exclude the corresponding
counter-example, $p_{i}$. In the latter case, we have shown that there is a
sequence of reachable states w.r.t. the corresponding invariant templates that
transition from $p$ to $p^{\prime}$. Therefore, $(p,p^{\prime})$ is in the
semantics of the body of the loop for every possible refinement of
$\mathsf{A}$. In this case, we return $\mathsf{false}$.

For the SMT queries that generate candidate invariants, one must be able to
describe the set of all invariants in $\mathcal{I}$ and express whether an
invariant includes a state in a decidable SMT theory. For the SMT queries that
check the validity of invariants at a point in the program to be decidable,
the SMT encoding of the program has to fit into a decidable SMT theory.

##  6\. Implementation of Syndicate

###  6.1. Templates

Consider the set of all ranking functions of the form:
$\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0)$, where
$a^{i}_{j}\in\mathbb{Z}$ and $x_{i}$ are program variables. This includes
linear ranking functions as well as more complicated ranking functions that
can be useful for non-linear assignment statements and complicated loop
guards. We can extend this template to include lexicographic ranking
functions, $\langle e_{1},\cdots,e_{n}\rangle$, where each $e_{k}$ is of the
form $\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0)$ for some
$i,j,n\in\mathbb{Z}$. Here $j$ is the number of variables in a program.
Bounding the absolute sum of the coefficients $a^{i}_{j}$ for each
lexicographic component, $e_{k}$, ensures that this expanded set of ranking
functions satisfies the conditions in Theorem 5.3. There are two parameters
when defining this template, $i$ and $n$. We define $T(i,n)$, to be a template
in this form with $i$ summands per lexicographic expression and $n$
lexicographic expressions. Our implementation supports ranking function
templates $T(i,n)$ for any values of $i$ and $n$. For an invariant template
that satisfies the conditions in Theorem 5.3, we use sets of states that can
be represented by a conjunction of linear constraints, of the form
$d_{0}+\sum_{j}d_{j}x_{j}\geq 0$ where $d_{j}\in\mathbb{Z}$. This template is
closed under intersection and we again bound the absolute sum of the
coefficients $d_{i}$, which ensures that there is no infinite descending
chain. In this section, $\mathcal{F}$ and $\mathcal{I}$ will refer to this
specific ranking function template and this specific invariant template
respectively.

###  6.2. Implementation of Subprocedures

get_candidate - This function returns an element of the set
$\Pi(\mathsf{t},\mathcal{F})$. Since every function in $\mathcal{F}$ is
bounded below by 0, this problem reduces to finding a function
$f\in\mathcal{F}$ that reduces on all of the pairs of states in $\mathsf{t}$.
We can accomplish this by solving the following SMT query:

$\displaystyle\bigwedge_{(s,s^{\prime})\in\mathsf{t}}\Big{(}\big{(}\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x_{j},0)\big{)}-\big{(}\sum_{i}\max(a^{i}_{0}+\sum_{j}a^{i}_{j}x^{\prime}_{j},0)\big{)}\geq
1\Big{)}$

Here, $s=(x_{0},\cdots x_{j})$ represents a program state with concrete
valuations of all program variables, and $a^{i}_{j}$ are variables
representing the coefficients of the ranking function. Note that having a
large under-approximation, $\mathsf{t}$, reduces the remaining size of the
search space of ranking functions, $\Pi(\mathsf{t},\mathcal{F})$. However,
this increases the size of the SMT query to generate a candidate ranking
function. To manage this tradeoff, we introduce an optimization where we use a
smaller set, $\mathsf{t}_{s}$ s.t. $\mathsf{t}_{s}\subset\mathsf{t}$, generate
the candidate using $\mathsf{t}_{s}$ and then check the generated
candidate,$f$, against the rest of the pairs of states in $\mathsf{t}$. As
soon as we find one element of $\mathsf{t}$ for which the ranking function
does not decrease, we add it to $\mathsf{t}_{s}$ and query the SMT again. We
repeat this process till we have found a function in
$\Pi(\mathsf{t},\mathcal{F})$ or the SMT query is unsatisfiable, meaning
$\Pi(\mathsf{t},\mathcal{F})$ is empty.

check - This function takes as input $f$ and $\mathsf{A}$. As discussed in
Section 5.4, using the over-approximation of the loop body defined by
$\llbracket\mathsf{A}\rrbracket$, we define variables representing the state
at the start of one iteration, $(x_{1},\cdots,x_{j})$, the end of the
iteration, $(x^{\prime}_{1},\cdots,x^{\prime}_{j})$, and at the exit of each
loop within the body of the outer loop, $(x_{1,j},\cdots,x_{i,j})$. Then, we
determine the satisfiability of the formula:
$f((x_{1},\cdots,x_{j}))-f((x^{\prime}_{1},\cdots,x^{\prime}_{j}))<1$. If this
formula is unsatisfiable, then we have proven the validity of $f$ because we
have already established that $f$ is bounded. If this formula is satisfiable,
then the algorithm continues to refine either $\mathsf{A}$ or $\mathsf{t}$.

get_cex - From the SMT query in check, we have found a satisfying assignment
to $(x_{1},\cdots,x_{n})$ and $(x^{\prime}_{1},\cdots,x^{\prime}_{n})$.
$\texttt{{\color[rgb]{0.0,0.0,1.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,1.0}{\small{get\\_cex}}}}(f,\mathsf{A})$
returns the counter-example $(p,p^{\prime})$, where $p=(x_{1},\cdots,x_{n})$
and $p^{\prime}=(x^{\prime}_{1},\cdots,x^{\prime}_{n})$. In our
implementation, since we defined check to define variables,
$(x_{1,j},\cdots,x_{n,j})$, for the states at the end of each inner loop,
instead of only returning $(p,p^{\prime})$, this function can return
$(p_{1},\cdots,p_{m})$, where $p_{1}=p$, $p_{m}=p^{\prime}$ and
$p_{i}=(x_{1,j},\cdots,x_{i,j})$ for all $i\in[1,m]$. This sequence of states
will be used to define refine to satisfy the properties defined in Section 5.

refine - As described in Section 5.4, when considering a program with one
loop, we use Equations 3 and 4 to generate and check the validity of candidate
invariants that exclude $(p_{1},\cdots,p_{m})$ from the over-approximation of
the transition relation of the loop. When considering multiple loops, since
Equation 5 can be a large SMT query and is often not required to find a useful
invariant, we try to refine the invariants for the loops in individual SMT
queries to exclude the state $p_{i}$ from $\mathsf{I}_{i}$. If we cannot
refine the invariants of any of the loops to exclude the corresponding
counter-example, we assume that the states $(p_{1},\cdots,p_{m})$ are
reachable. This may not be true, because there could be a way to refine
multiple invariants simultaneously to exclude a non-empty subset of the states
$(p_{1},\cdots,p_{m})$. Since $(p,p^{\prime})$ may be not be in the exact
transition relation of the loop, instead of adding $(p,p^{\prime})$ to
$\mathsf{t}$ we add it to a new set, $\mathsf{t}^{?}$. $\mathsf{t}^{?}$
contains pairs of states for which we are unsure whether or not they are
elements of $\llbracket\mathsf{P}\rrbracket$. Whenever we refine an invariant
for any loop in the program, we check whether the current annotated program,
$\mathsf{A}$, can prove that any states in $\mathsf{t}^{?}$ are unreachable.
If so, we remove those states from $\mathsf{t}^{?}$. When generating candidate
ranking functions, instead of using $\mathsf{t}$, we use
$\mathsf{t}\cup\mathsf{t}^{?}$. So, the generate candidate phase changes to
output a function, $f\in\mathcal{F}$ that decreases and is bounded on all
states in $\mathsf{t}\cup\mathsf{t}^{?}$. When no candidate ranking function
is found, the algorithm terminates. Since $\mathsf{t}^{?}$ may contain
unreachable pairs of states, this algorithm can terminate without finding a
valid ranking function even if one exists in $\mathcal{F}$ that can be proved
by an annotated program that has invariants in $\mathcal{I}$. The use of
$\mathsf{t}^{?}$ makes our implementation of the algorithm described in
Section 5 incomplete. We further introduce some approximations in our
implementation, by limiting the number of iterations of generating candidate
invariants within the refine procedure and limiting the number of times we
call refine without changing our candidate ranking function. When these
approximations are used, the counter-examples from checking the validity of
the ranking functions, $(p,p^{\prime})$, are added to $\mathsf{t}^{?}$ instead
of $\mathsf{t}$.

##  7\. Evaluation

We implement Syndicate in Python. As described in Section 6.1, for the
template of invariants, we use a set of linear inequalities, specifically of
the form of $d_{0}+\sum d_{j}x_{j}\geq 0$, where $d_{j}\in\mathbb{Z}$. For
ranking functions, recall that we defined $T(i,n)$ to be a template with $i$
summands per lexicographic expression and $n$ lexicographic expressions. For
our evaluation, we consider 5 templates with different values of $i,n$, i.e.,
$\mathcal{F}_{1}=T(1,1),\;\mathcal{F}_{2}=T(1,2),\;\mathcal{F}_{3}=T(1,3),\;\mathcal{F}_{4}=T(2,1),\text{and}\;\mathcal{F}_{5}=T(2,2)$
Further, for all our experiments, we use 200 randomly generated initial
traces. Syndicate expects Java programs as inputs and returns a ranking
function and the corresponding loop invariants if it proves termination. We
use Z3-Java API to check the validity of the ranking functions and the loop
invariants. All experiments are run on a 2.50 GHz 16 core 11th Gen Intel
i9-11900H CPU with a main memory of 64 GB. For all our tests, we use a timeout
of 120 s. When computing the average time, we use the time taken to be 120
seconds for instances that timeout.

#### Benchmarks

We collect 168 challenging programs as benchmarks from the Term-crafted set of
SV-COMP (Beyer, 2020), the Aprove_09 set from TermComp (Giesl et al., 2019),
and $\nu$Term-advantage from $\nu$Term (Giacobbe et al., 2022). These
benchmarks contain integer programs, with linear and non-linear assignments
and loop guards, non-determinism, nested loops of maximum depth 3, and
sequential loops. Except for random number generators, our implementation
currently does not support function calls. However, the theory can be directly
extended to support function calls by inlining them. The programs were
originally in C but were also translated to Java by (Giacobbe et al., 2022).
The experiments for Syndicate and $\nu$Term are run on the Java version while
the experiments for Aprove, Ultimate, and DynamiTe are run on the equivalent C
benchmarks.

###  7.1. Comparison with State-of-the-art Termination Analysis Tools

|  $\\#$ Proved | Avg. Time (s)
---|---|---
Syndicate | 151 | 15.96
Ultimate | 144 | 23.69
Aprove | 142 | 22.31
DynamiTe | 126 | 53.04

(a) Total number of benchmarks - 168

|  $\\#$ Proved | Avg. Time (s)
---|---|---
Syndicate | 104 | 27.55
$\nu$Term | 95 | 33.13

(b) Total number of benchmarks - 128

Table 1. Total number of benchmarks proved and the average time for state-of-
the-art termination analysis algorithms using a timeout of 2 minutes.
Syndicate takes 32.6% less average time than Ultimate, 28.5% less than Aprove,
69.9% less than DynamiTe, and 16.8% less than $\nu$Term.

We compare Syndicate against the following state-of-the-art tools for
termination analysis.

  1. (1)

Ultimate (Heizmann et al., 2014) decomposes programs into smaller sub-programs
and constructs ranking functions for these sub-programs. After finding each
ranking function, it checks whether the current set of sub-programs captures
the behavior of the entire loop.

  2. (2)

Aprove (Giesl et al., 2017) is an ensemble of several proof techniques,
including termination proofs through reduction orders and dependency pairs.

  3. (3)

DynamiTe (Le et al., 2020) tries to prove the non-termination of programs by
finding recurrent sets, failing which it generates a counter-example that is
then used to find candidate ranking functions. To finally prove termination,
the synthesis of invariants is outsourced to an external invariant synthesis
algorithm, DIG (Nguyen et al., 2014).

  4. (4)

${\nu}$Term (Giacobbe et al., 2022) trains a neural network from randomly
generated traces to maximize the difference between the output of two
consecutive states. The trained model is then treated as a candidate ranking
function.

Figure 3. Percentage of benchmarks proved terminating with growing running
time. Syndicate is the overall best, except for easier benchmarks as it takes
extra time to generate the initial 200 traces.

Figure 4. No. of benchmarks proved terminating by Syndicate but not by the
existing tool and vice-versa. The total number of benchmarks used is 128 for
comparison with $\nu$Term and 168 for all others.

For comparison to the above tools, Syndicate tests for the termination of a
given benchmark using all $5$ templates ($\mathcal{F}_{i}$) in parallel and
stops as soon as one of the templates proves the termination. Note that all
the existing tools also have a parallel implementation. In Table 1(a), we
present the total number of benchmarks that each tool could prove and the
average time taken to run the tools on a benchmark. The efficacy of Syndicate
is demonstrated by the fact that it proves the most number of benchmarks and
takes the least amount of average time. It is noteworthy that although state-
of-the-art tools like Aprove employ an ensemble of several methods to prove
termination, Syndicate surpasses them by relying solely on ranking functions
to argue for program termination. Further, $\nu$Term cannot handle the
benchmarks with sequential loops or calls to random number generators and thus
supports only a subset of the total benchmarks. So, we compare against
$\nu$Term in Table 1(b) on 128 benchmarks. Note that we can exactly match the
template of ranking functions used by $\nu$Term. So, for this experiment, we
fix the template both for $\nu$Term and Syndicate to $\mathcal{F}_{4}$.
$\nu$Term uses 1000 initial traces for best baseline performance.

In Fig. 4, we show a cactus plot where the y-axis shows the percentage of
total benchmarks proved terminating within the time on the x-axis. The x-axis
is in the log scale. Syndicate achieves the overall fastest average running
time compared to all other tools with minimal timeouts and leads on the cactus
plot. In the initial 2.2s of the plot, Aprove is better than Syndicate. This
is because Syndicate incurs a fixed cost since it uses program traces to
generate candidate ranking functions. On the other hand, Aprove is a
collection of several termination analysis techniques, due to which it can
solve the easy benchmarks quickly. However, Syndicate surpasses Aprove in the
long run and solves relatively more challenging benchmarks faster. In Fig. 4,
we present the number of benchmarks that Syndicate could prove terminating,
but the other tools could not, and also the number of benchmarks the existing
tools could prove terminating, and Syndicate could not within the timeout
limit. Syndicate can prove termination for significantly more benchmarks as
compared to each of the existing tools. This highlights the distinct
advantages and capabilities of Syndicate’s synergistic approach. Note that the
comparison with $\nu$Term is only using 128 benchmarks.

###  7.2. Case Studies

⬇

1 int x = y + 42;

2 while (x >= 0) {

3 y = 2 * y - x;

4 x = (y + x) / 2;

5 }

(a) Not proved by Aprove and Ultimate

⬇

1 int a = 0, b = 0;

2 while (a * b <= n || a * b <= m) {

3 a = a + 1;

4 b = b + 1;

5 }

(b) Not proved by any of Aprove, Ultimate, DynamiTe, and $\nu$-Term

Figure 5. Benchmarks for Case Studies proved terminating by Syndicate.

To shed more light on the efficacy of Syndicate, we discuss two non-trivial
programs from our benchmarks where some of the existing tools fail to prove
termination within the timeout while Syndicate succeeds in just 1.8s and 5.4s
respectively. Specifically, we compare more qualitatively against DynamiTe and
$\nu$Term, which most closely resemble parts of Syndicate. Consider the
program in Fig 5(a). To prove its termination, one tries to prove that $x$
reduces in successive iterations, which is not trivial. A non-trivial
algebraic rewriting of the assignment expressions in lines 4 and 5 reveals
that both $x$ and $y$ decrease by the value $x-y$ computed at the beginning of
the iteration in each iteration. Furthermore, one needs an invariant at least
as strong as $x-y>0$ to show that $x$ always reduces. Unlike some other
termination analysis tools, Syndicate does not rely on algebraic rewriting to
infer the ranking functions and invariants. Instead, it uses traces to
generate candidates and subsequently uses and SMT solver to verify its
validity. Syndicate solves it in just 1.8s owing to its synergistic search for
a termination argument and results in $f^{*}\equiv\max(x+1,0)$ and
$\mathsf{I}^{*}\equiv x-y\geq 1$. Note that DynamiTe, which also relies on
traces to come up with candidate ranking functions, is 5$\times$ slower and
takes 11.9s to solve the problem. This is possibly because the invariant
generation in DynamiTe is outsourced to DIG but does not explicitly guide the
invariant search. Invariants other than $\mathsf{I}^{*}$ (like $x-y\geq 42$ or
even stronger) may also prove the validity of $f^{*}$ but a naive unguided
search for invariants results in longer runtime. Further, $\nu$Term can also
prove the termination in 2.56s, but its reliance on heuristically guessed
invariants is not generalizable.

Similarly, Fig. 5(b) shows another non-trivial example consisting of non-
linear expressions and disjunctive boolean guards, for which none of the
existing tools used in our experiments could prove termination. Syndicate,
however, generates a valid lexicographic ranking function
$\langle\max(n-2m+a-4b+1,0),\max(m+a-2b+6,0)\rangle$ and loop invariant $a\geq
b$ that proves that the generated ranking function is valid in just 5.4s.
Notably, even DynamiTe, which also uses trace-based methods to create ranking
functions, fails to verify the termination even on increasing the timeout to 5
minutes. Our experiments with the invariant generation engine of DynamiTe
(DIG) indicate that it takes a long time to produce invariants that are useful
for proving the validity of the generated ranking functions. Further, even
though there is a valid ranking function in the template used by $\nu$Term, it
fails to find it because of its inability to guess the required invariants.
These examples demonstrate that a synergistic search can increase the number
of benchmarks that can be proved terminating and also significantly reduce the
analysis runtime by finding ranking functions from traces and by guiding the
search for invariants just strong enough to prove it.

###  7.3. Ablation Studies

(a) B-synergy1 and B-synergy2

(b) B-combined

Figure 6. Percentage of benchmarks proved terminating with growing running
time. Fig 6(a) uses 168 benchmarks and Fig 6(b) uses 153 benchmarks.

(a) Syndicate vs B-synergy1

(b) Syndicate vs B-synergy2

Figure 7. No. of benchmarks proved terminating by Syndicate but not by the
baselines out of 168 benchmarks.

As highlighted in the introduction, we show that the two-way synergy used in
Syndicate (invariant guiding the ranking function and vice-versa) is better
than either one of them individually in terms of the number of proved
benchmarks and the average runtime. We also show that the synergistic
technique significantly outperforms searching for the ranking function and the
invariant using a single query. The following experiments also show that the
benefit of the synergy is independent of the exact instantiation of the
template for ranking functions. For this, we implemented 3 baselines -
B-synergy1, B-synergy2, and B-combined. First, B-synergy1 does not use the
counter-examples from checking the validity of candidate invariants to guide
the generation of new candidate ranking functions. This demonstrates the
effect of having only the ranking function guide the invariant search. Second,
B-synergy2 does not use the counter-examples from checking the validity of
candidate ranking functions to guide the generation of new candidate
invariants. This demonstrates the effect of having only the invariant guide
the ranking function search. Third, B-combined searches for both ranking
function and invariant with a single monolithic query. In the following
experiments, the baselines use the same template for invariants as Syndicate.
B-synergy1 and B-synergy2 are instantiated with the 5 ranking function
templates $\mathcal{F}_{i}$ described in Section 7. B-combined is only
instantiated with $\mathcal{F}_{1}$ because $\mathcal{F}_{1}$ is the simplest
template and B-combined does not scale well even with $\mathcal{F}_{1}$.

Template | Syndicate | B-synergy1 | B-synergy2
---|---|---|---
$\mathcal{F}_{1}$ | 94 | 85 | 83
$\mathcal{F}_{2}$ | 142 | 134 | 128
$\mathcal{F}_{3}$ | 146 | 138 | 137
$\mathcal{F}_{4}$ | 121 | 112 | 109
$\mathcal{F}_{5}$ | 131 | 127 | 110
Table 2. The number of benchmarks out of 168 proved by Syndicate and baselines
for different templates.

In Fig. 6(a), we show the percentage benchmarks proved with growing time for
Syndicate, B-synergy1, and B-synergy2 in the case of template
$\mathcal{F}_{2}$. We can see that both baselines perform worse than
Syndicate, indicating that using both the counter-examples from the invariant
search and the counter-examples from the ranking function search to guide each
other increases the number of benchmarks proved. The graphs for other
templates are similar and can be found in Appendix C. In Table 2, we show the
numbers of benchmarks proved by Syndicate and B-synergy1 and B-synergy2 using
each template. There is up to 8% improvement over B-synergy1 and up to 19%
improvement over B-synergy2. In Figs. 7(a), 7(b), we show the number of
benchmarks that are uniquely solved by B-synergy(i) as compared to Syndicate.
We can see that Syndicate is significantly better than both the baselines. We
observe that in a few benchmarks, the baselines are better than Syndicate due
to the non-determinism involved in guessing the candidates. In Fig. 6(b), we
compare the Syndicate to B-combined, using $\mathcal{F}_{1}$ for both. Our
implementation of B-combined only handles non-nested loops, so we use 153
benchmarks to evaluate B-combined. B-combined can solve only 31 of the total
benchmarks. It solves these quickly because of less number of iterations
needed but times out on relatively more complicated benchmarks because there
is a large search space for the query. This shows that such a strategy cannot
scale as the complexity of the benchmarks grows.

##  8\. Related Works

Termination Analysis. Numerous techniques have been designed to reason about
termination (Giacobbe et al., 2022; Urban et al., 2016; Cook et al., 2006; Xie
et al., 2017; Le et al., 2020; Gonnord et al., 2015; Podelski and Rybalchenko,
2004; Bradley et al., 2005b) and non-termination (Le et al., 2020; Heizmann et
al., 2014; Velroyen and Rümmer, 2008; Han and He, 2023; Chen et al., 2014) of
programs. Synthesizing ranking functions is one well-established way of
proving termination. As discussed in Section 1, there are techniques that
separate the search for a valid ranking function and an invariant strong
enough to prove it (Urban et al., 2016; Giacobbe et al., 2022; Le et al.,
2020; Cook et al., 2006). These can handle a wide variety of programs but do
not provide completeness guarantees. There are techniques that provide
completeness guarantees but handle a restricted class of programs(Gonnord et
al., 2015; Podelski and Rybalchenko, 2004; Bradley et al., 2005a; Heizmann et
al., 2014). For example, (Podelski and Rybalchenko, 2004; Bradley et al.,
2005a) propose complete methods to find linear ranking functions and linear
invariants to prove the termination of linear programs. There are also
techniques that provide completeness guarantees and handle complex programs
(Unno et al., 2021, 2023), but these techniques encode an over-approximation
of the reachable states and ranking functions in a single formula. (Unno et
al., 2023) is more scalable, but it relies on information from searching for
non-termination arguments to make the search for termination arguments
scalable. Syndicate focuses only on termination and proves termination by
synthesizing ranking functions and invariants in different sub-routines that
exchange important information. It can handle a wide variety of programs and
also offers relative completeness guarantees while maintaining efficiency.

Guided search for invariants. Several previous works (Nguyen et al., 2014,
2022) have focused on identifying loop invariants. These works, however, aim
to discover loop invariants without being specifically guided by a particular
property. It has been established (Furia and Meyer, 2010; Galeotti et al.,
2015; Miltner et al., 2020; Padon et al., 2022; Garg et al., 2014) that
proving properties does not always need the identification of the strongest
invariants. Instead, it is often more efficient to search for invariants that
specifically contribute to proving the desired property. (Welp and Kuehlmann,
2014) leverages the concept of Property Directed Reachability (Bradley, 2011)
to infer invariants that are directed toward achieving the goal of proving the
input verification condition. (Miltner et al., 2020) proposes a
counterexample-driven algorithm for inferring invariants sufficient to imply
some desired specifications. Our search for invariant is also guided by a
goal, which is to prove the validity of a ranking function. But we do not have
a target ranking function. So, we synergistically guide the search for
invariants and ranking functions.

Counter-example guided learning. Many frameworks like CEGIS (Solar-Lezama et
al., 2008; Clarke et al., 2000; Gupta et al., 2020; Preiner et al., 2017) work
on the methodology of using counter-examples to guide their search for
specific candidates (programs, abstractions etc.) that satisfy a fixed
property. Our approach, while similar, poses a greater challenge as we are
simultaneously searching for both a valid ranking function and an invariant
that can prove it in seperate CEGIS loops that guide each other.

##  9\. Conclusion

We developed a general recipe called Syndicate for automated termination
analysis based on a synergistic synthesis of invariants and ranking functions.
Syndicate can be instantiated with different templates for invariants and
ranking functions, is relatively complete, and can handle complex programs. We
provided a specific instantiation of Syndicate where invariants are
represented as linear inequalities and ranking functions are lexicographic
expressions, with sums of max terms. We empirically showed that this specific
instantiation can prove the termination of more benchmarks than state-of-the-
art termination analysis tools and in a faster time. We leave instantiation of
Syndicate with more complex templates and the development of an algorithm to
automatically discover suitable templates for a given program as future works.

## References

  * (1)
  * Beyer (2020) Dirk Beyer. 2020.  Advances in Automatic Software Verification: SV-COMP 2020. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Armin Biere and David Parker (Eds.). Springer International Publishing, Cham, 347–367.
  * Bradley (2011) Aaron R. Bradley. 2011.  SAT-Based Model Checking without Unrolling. In _Verification, Model Checking, and Abstract Interpretation_ , Ranjit Jhala and David Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 70–87.
  * Bradley et al. (2005a) Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005a.  Linear Ranking with Reachability. In _Computer Aided Verification_ , Kousha Etessami and Sriram K. Rajamani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 491–504.
  * Bradley et al. (2005b) Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005b.  Termination of Polynomial Programs. In _Verification, Model Checking, and Abstract Interpretation_ , Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113–129.
  * Chen et al. (2014) Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter O’Hearn. 2014.  Proving Nontermination via Safety. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 156–171.
  * Clarke et al. (2000) Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000.  Counterexample-Guided Abstraction Refinement. In _Computer Aided Verification_ , E. Allen Emerson and Aravinda Prasad Sistla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 154–169.
  * Cook et al. (2006) Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006.  Termination Proofs for Systems Code. In _Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Ottawa, Ontario, Canada) _(PLDI ’06)_. Association for Computing Machinery, New York, NY, USA, 415–426.  https://doi.org/10.1145/1133981.1134029
  * de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008.  Z3: An Efficient SMT Solver. In _TACAS_ _(Lecture Notes in Computer Science, Vol. 4963)_. Springer, 337–340.
  * Furia and Meyer (2010) Carlo Alberto Furia and Bertrand Meyer. 2010.  _Inferring Loop Invariants Using Postconditions_.  Springer Berlin Heidelberg, Berlin, Heidelberg, 277–300.  https://doi.org/10.1007/978-3-642-15025-8_15
  * Galeotti et al. (2015) Juan P. Galeotti, Carlo A. Furia, Eva May, Gordon Fraser, and Andreas Zeller. 2015.  Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking.  _IEEE Transactions on Software Engineering_ 41, 10 (2015), 1019–1037.  https://doi.org/10.1109/TSE.2015.2431688
  * Garg et al. (2014) Pranav Garg, Christof Löding, P. Madhusudan, and Daniel Neider. 2014.  ICE: A Robust Framework for Learning Invariants. In _Computer Aided Verification_ , Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 69–87.
  * Giacobbe et al. (2022) Mirco Giacobbe, Daniel Kroening, and Julian Parsert. 2022.  Neural Termination Analysis. In _Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ (Singapore, Singapore) _(ESEC/FSE 2022)_. Association for Computing Machinery, New York, NY, USA, 633–645.  https://doi.org/10.1145/3540250.3549120
  * Giesl et al. (2017) Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2017.  Analyzing Program Termination and Complexity Automatically with AProVE.  _J. Autom. Reason._ 58, 1 (jan 2017), 3–31.  https://doi.org/10.1007/s10817-016-9388-y
  * Giesl et al. (2019) Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. 2019.  The Termination and Complexity Competition. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.). Springer International Publishing, Cham, 156–166.
  * Gonnord et al. (2015) Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015.  Synthesis of Ranking Functions Using Extremal Counterexamples.  _SIGPLAN Not._ 50, 6 (jun 2015), 608–618.  https://doi.org/10.1145/2813885.2737976
  * Gupta et al. (2020) Shubhani Gupta, Abhishek Rose, and Sorav Bansal. 2020.  Counterexample-Guided Correlation Algorithm for Translation Validation.  _Proc. ACM Program. Lang._ 4, OOPSLA, Article 221 (nov 2020), 29 pages.  https://doi.org/10.1145/3428289
  * Han and He (2023) Zhilei Han and Fei He. 2023.  Data-driven Recurrent Set Learning For Non-termination Analysis. In _2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)_. 1303–1315.  https://doi.org/10.1109/ICSE48619.2023.00115
  * Heizmann et al. (2014) Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014.  Termination Analysis by Learning Terminating Programs.  https://doi.org/10.1007/978-3-319-08867-9_53
  * Le et al. (2020) Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen. 2020.  DynamiTe: Dynamic Termination and Non-Termination Proofs.  _Proc. ACM Program. Lang._ 4, OOPSLA, Article 189 (nov 2020), 30 pages.  https://doi.org/10.1145/3428257
  * Miltner et al. (2020) Anders Miltner, Saswat Padhi, Todd Millstein, and David Walker. 2020.  Data-Driven Inference of Representation Invariants. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ (London, UK) _(PLDI 2020)_. Association for Computing Machinery, New York, NY, USA, 1–15.  https://doi.org/10.1145/3385412.3385967
  * Nguyen et al. (2014) Thanhvu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. 2014.  DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants.  _ACM Trans. Softw. Eng. Methodol._ 23, 4, Article 30 (sep 2014), 30 pages.  https://doi.org/10.1145/2556782
  * Nguyen et al. (2022) ThanhVu Nguyen, KimHao Nguyen, and Hai Duong. 2022.  SymInfer: Inferring Numerical Invariants using Symbolic States. In _2022 IEEE/ACM 44th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion)_. 197–201.  https://doi.org/10.1145/3510454.3516833
  * Padon et al. (2022) Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022.  Induction Duality: Primal-Dual Search for Invariants.  _Proc. ACM Program. Lang._ 6, POPL, Article 50 (jan 2022), 29 pages.  https://doi.org/10.1145/3498712
  * Podelski and Rybalchenko (2004) Andreas Podelski and Andrey Rybalchenko. 2004.  A Complete Method for the Synthesis of Linear Ranking Functions. In _Verification, Model Checking, and Abstract Interpretation_ , Bernhard Steffen and Giorgio Levi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 239–251.
  * Preiner et al. (2017) Mathias Preiner, Aina Niemetz, and Armin Biere. 2017.  Counterexample-Guided Model Synthesis. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Axel Legay and Tiziana Margaria (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 264–280.
  * Solar-Lezama et al. (2008) Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. 2008.  Sketching Concurrent Data Structures.  _SIGPLAN Not._ 43, 6 (jun 2008), 136–148.  https://doi.org/10.1145/1379022.1375599
  * Unno et al. (2023) Hiroshi Unno, Tachio Terauchi, Yu Gu, and Eric Koskinen. 2023.  Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.  _Proc. ACM Program. Lang._ 7, POPL, Article 72 (jan 2023), 30 pages.  https://doi.org/10.1145/3571265
  * Unno et al. (2021) Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021.  Constraint-Based Relational Verification. In _Computer Aided Verification_ , Alexandra Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 742–766.
  * Urban et al. (2016) Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016.  Synthesizing Ranking Functions from Bits and Pieces. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Marsha Chechik and Jean-François Raskin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 54–70.
  * Velroyen and Rümmer (2008) Helga Velroyen and Philipp Rümmer. 2008.  Non-termination Checking for Imperative Programs. In _Tests and Proofs_ , Bernhard Beckert and Reiner Hähnle (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 154–170.