$\widehat{\pi}$ be the prefix of $\pi$ that ends at $n$. We prove by induction
on the length of $\widehat{\pi}$ that $n$ is also reached along $\pi^{\prime}$
and the program state computed at $n$ along $\pi$ is the same as the state at
$n$ along $\pi^{\prime}$. The proof crucially uses the fact that the guards of
all statements in $\mathsf{T}_{N}^{p}$ that do not correspond to statements in
nodes along $\pi$ evaluate to $\mathsf{False}$. The reasons for this are (i)
every such guard has a conjunct that is the negation of some branch condition
$b$ that evaluates to $\mathsf{True}$ along $\pi$, (ii) the consequence of the
no-overwriting property stated above, and (iii) sequencing of statements in
topological index order in $\mathsf{T}_{N}^{p}$. In particular, (ii) and (iii)
above ensure that the values of all variables/array elements used in the
branch node $b$ along $\pi$ are the same as the corresponding values used in
$b$ along $\pi^{\prime}$.

The converse direction of the proof is similar.

####  4.5.2 Reordering the Peels

We now reorder the statements in the program $\mathsf{T}_{N}^{p}$ such that
all guarded statements corresponding to peels of loops are executed after all
other guarded statements. However, the relative ordering among the guarded
statements corresponding to peels is preserved. We use $\mathsf{T}_{N}^{o}$ to
denote the program obtained after this reordering.

######  Example 7.

Continuing with the canonicalized program $\mathsf{T}_{N}^{p}$ shown in Tab.
1(b), the reordered program $\mathsf{T}_{N}^{o}$ is shown in Tab. 1(c). The
line numbers follow the same pattern described in Example 6. Notice that in
$\mathsf{T}_{N}^{o}$ the guarded statements corresponding to peels at lines
$5^{\prime}$, $9^{\prime}$ and $12^{\prime}$ appear after all other statements
in the program.

Let $vA$ be a variable/array in $\mathsf{P}_{N}^{p}$ that is not identified as
affected by function ComputeAffected. The following lemmas establish that if
programs $\mathsf{T}_{N}^{p}$ and $\mathsf{T}_{N}^{o}$ are executed from the
same state $\sigma$, they always compute the same value of $vA$. Specifically,
Lemma 14 shows that all data dependencies that potentially have a bearing on
the value of $vA$ are the same in $\mathsf{T}_{N}^{p}$ and
$\mathsf{T}_{N}^{o}$. Lemma 15 uses this to show that the value of $vA$
computed by $\mathsf{T}_{N}^{p}$ and $\mathsf{T}_{N}^{o}$ are the same. For
clarity of exposition in the following discussion, when we say that there is a
data dependence path from $n_{i}$ to $n_{j}$ in a program, we mean that there
is a path from $n_{i}$ to $n_{j}$ in the DDG of the program. Similarly, when
we say that there is a control dependence path from $n_{i}$ to $n_{j}$, we
mean that there is a data dependence path from $n_{i}$ to a conditional branch
node within whose scope $n_{j}$ lies.

######  Lemma 14.

Let $vA$ be a scalar variable/array that is absent in $\mathsf{AffectedVars}$
when ComputeAffected is invoked on $\mathsf{P}_{N}^{p}$. Let $n$ be a node in
$\mathsf{P}_{N}^{p}$ such that $vA\in\mathit{def}(n)$. For every node
$n^{\prime}$ in $\mathsf{P}_{N}^{p}$, there is a data/control dependence path
from $n^{\prime}$ to $n$ in $\mathsf{T}_{N}^{p}$ iff there exists such a path
in $\mathsf{T}_{N}^{o}$.

Proof: Consider nodes $n$ and $n^{\prime}$ in $\mathsf{P}_{N}^{p}$ (hence also
in $\mathsf{T}_{N}^{p}$ and $\mathsf{T}_{N}^{o}$). We consider two cases.

  1. 1.

Suppose there is a data/control dependence path from $n^{\prime}$ to $n$ in
$\mathsf{T}_{N}^{p}$. From our construction of $\mathsf{T}_{N}^{p}$, we know
that there exists such a data/control dependence path in $\mathsf{P}_{N}^{p}$
as well. We now show that such a data/control dependence path also exists in
$\mathsf{T}_{N}^{o}$ by considering two sub-cases.

    1. (a)

Suppose $n$ is a non-peeled node in $\mathsf{P}_{N}^{p}$. Since $vA$ is not
identified as affected, by the not-affected property (Lemma 12), we have that
$n^{\prime}$ is not a peeled node. Therefore, both $n$ and $n^{\prime}$ are
non-peeled nodes. Since the relative ordering of all non-peeled nodes is
preserved by our reordering transformation, the data/control dependence
between $n$ and $n^{\prime}$ continues to exist in $\mathsf{T}_{N}^{o}$ as
well.

    2. (b)

Suppose $n$ is a peeled node in $\mathsf{P}_{N}^{p}$. If $n^{\prime}$ is also
a peeled node, then since the relative ordering among the peeled nodes is
preserved by reordering, the data/control dependence between $n$ and
$n^{\prime}$ continues to exist in $\mathsf{T}_{N}^{o}$. On the other hand, if
$n^{\prime}$ is a non-peeled node, since all non-peeled nodes precede all
peeled nodes after reordering, the data/control dependence exists in
$\mathsf{T}_{N}^{o}$ in this case as well.

  2. 2.

Suppose there is a data/control dependence path from $n^{\prime}$ to $n$ in
$\mathsf{T}_{N}^{o}$. We show that such a dependence path exists in
$\mathsf{T}_{N}^{p}$ by considering the following sub-cases.

    1. (a)

If both $n^{\prime}$ and $n$ are non-peeled (resp. peeled) nodes, then since
reordering does not change the relative ordering of the non-peeled (resp.
peeled) nodes, the dependence is present in $\mathsf{T}_{N}^{p}$.

    2. (b)

The case where $n$ is a non-peeled node and $n^{\prime}$ is peeled node cannot
arise, since all non-peeled nodes appear before peeled nodes in
$\mathsf{T}_{N}^{o}$.

    3. (c)

If $n^{\prime}$ is a non-peeled node and $n$ is a peeled node, there are two
further sub-cases. If $n^{\prime}$ is ordered before $n$ in
$\mathsf{T}_{N}^{p}$ then the dependence is present in $\mathsf{T}_{N}^{p}$ as
well. Otherwise, we ask if the dependence from $n^{\prime}$ to $n$ in
$\mathsf{T}_{N}^{o}$ is a read-after-write or write-after-write. Since $n$ is
ordered before $n^{\prime}$ in $\mathsf{T}_{N}^{p}$, by the no-overwriting
property (Lemma 4), both $n$ and $n^{\prime}$ cannot update the same renamed
variable. Therefore, the dependence from $n^{\prime}$ to $n$ in
$\mathsf{T}_{N}^{o}$ cannot be write-after-write, and hence must be read-
after-write. This requires a variable/array element in $\mathit{uses}(n)$ to
also be present in $\mathit{def}(n^{\prime})$. Such a variable/array element
must have been updated (if at all) prior to its use in node $n$. Once again,
by the no-overwriting property, this variable/array element cannot be updated
by $n^{\prime}$, which appears after $n$ in $\mathsf{T}_{N}^{p}$. This
completes the proof.

######  Lemma 15.

Let $vA$ be a scalar variable/array that is absent in $\mathsf{AffectedVars}$
upon invocation of ComputeAffected on $\mathsf{P}_{N}^{p}$. If
$\mathsf{T}_{N}^{p}$ and $\mathsf{T}_{N}^{o}$ are executed from the same state
$\sigma$, then $vA$ has the same value on termination of both programs.

Proof: Follows from Lemma 14 and the fact that reordering does not change the
individual guarded statements in the canonicalized program
$\mathsf{T}_{N}^{p}$.

####  4.5.3 De-canonicalizing the Reordered Program

Recall that our aim is to decompose the program $\mathsf{P}_{N}^{p}$ into two
program fragments, the program $\mathsf{P}_{N-1}$ and the difference program
$\partial\mathsf{P}_{N}$. We have seen above that the reordering step already
achieves the purpose of moving the guarded statements corresponding to peels
to the end of the program, providing a good candidate for the difference
program $\partial\mathsf{P}_{N}$. However, the part of the reordered program
that precedes the guarded statements corresponding to peels may not have
syntactic similarity with $\mathsf{P}_{N-1}$ in general. In order to remedy
this situation, we now “undo” the canonicalization process (as described in
Sect. 4.5.1) that allowed us to view the program $\mathsf{P}_{N}^{p}$ as a
linear sequence of guarded statements. Specifically, we transform the guarded
statements back to statements of the form that were present in
$\mathsf{P}_{N}^{p}$ to begin with. We do this separately for the guarded
statements corresponding to peels, and for the part of $\mathsf{T}_{N}^{o}$
that precedes these, so that we obtain a program fragment that is
syntactically similar to $\mathsf{P}_{N-1}$ followed by a difference program.
In the subsequent discussion, we call the resulting de-canonicalized program
$\mathsf{P}_{N}^{o}$.

######  Example 8.

Consider the reordered program $\mathsf{T}_{N}^{o}$ from the example shown in
Tab. 1(c). The program $\mathsf{P}_{N}^{o}$ shown in Tab. 1(d) is obtained by
de-canonicalization. The line numbers follow the pattern similar to the
program $\mathsf{P}_{N}^{p}$ as described in Example 6. It is worth noticing
that, the statements corresponding to peels of loops appear after all other
statements in $\mathsf{P}_{N}^{o}$ and part of program $\mathsf{P}_{N}^{o}$
that precedes the peels is syntactically similar to $\mathsf{P}_{N-1}$.

Notice that after de-canonicalization, there may be more conditional branch
nodes in the CFG of $\mathsf{P}_{N}^{o}$ as compared to the CFG of
$\mathsf{P}_{N}^{p}$ but fewer conditional branch nodes as compared to the CFG
of $\mathsf{T}_{N}^{o}$.

######  Lemma 16.

Let $\mathsf{P}_{N}^{o}$ be the de-canonicalized version of
$\mathsf{T}_{N}^{o}$. Let $n$ be a node corresponding an assignment statement
in the CFG of $\mathsf{T}_{N}^{o}$ (and hence $\mathsf{P}_{N}^{o}$). Let $\pi$
(resp. $\pi^{\prime}$) be a path in the collapsed CFG of $\mathsf{T}_{N}^{o}$
(resp. $\mathsf{P}_{N}^{o}$) starting from the state $\sigma$. Then the
following hold.

  1. 1.

$n$ is reached along $\pi$ iff $n$ is also reached along $\pi^{\prime}$.

  2. 2.

The program state $\sigma_{n}$ is computed at node $n$ along $\pi$ iff the
program state $\sigma_{n}$ is computed at node $n$ along $\pi^{\prime}$.

Proof: The proof is similar to that shown in Lemma 13.

####  4.5.4 Peels of Loops as the Difference Program

Recall from Sect. 4.4 that $\mathsf{P}_{{N}}^{\star}$ is effectively
$\mathsf{P}_{N}$ with the peels removed. This is exactly what we get by de-
canonicalizing the part of $\mathsf{T}_{N}^{o}$ that precedes the guarded
statements corresponding to peels. If we call the de-canonicalized version of
the guarded statements corresponding to peels as
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ then $\mathsf{P}_{N}^{o}$ can be written
as $\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$.

It turns out that $\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ can be constructed
directly from $\mathsf{P}_{N}$ without having to go through canonicalization,
reordering and de-canonicalization. We now describe how to do this. Recall
from Sect. 4.2 that $\mathsf{PeelNodes}$ denotes the set of peeled nodes in
$\mathsf{P}_{N}^{p}$. Let $\mathsf{CondNodes}$ be the set of all non-peeled
conditional branch nodes $b$ such that there is a peeled node $n$ within the
scope of the branch $b$. In other words, if $d$ denotes the immediate post-
dominator of $b$, there is a path from $b$ to $d$ that passes through $n$. We
define $\mathit{Locs}$ to be the set
$\mathsf{PeelNodes}\cup\mathsf{CondNodes}$. Only these nodes in the CFG of
$\mathsf{P}_{N}^{p}$ are relevant for the construction of
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$. Therefore, we construct
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ by replacing the labels of all other
nodes in the CFG of $\mathsf{P}_{N}^{p}$ by $\mathsf{skip}$. Recall that
$\mathsf{skip}$ is a syntactic shorthand for x = x; for a variable x, as
discussed before. Since a sequence of $\mathsf{skip}$ statements can be
collapsed without changing the program semantics, we use
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ to denote the program obtained after
this optimization.

######  Example 9.

Consider the peeled program $\mathsf{P}_{N}^{p}$ shown in Tab. 1(a). The
program has a non-peeled conditional branch statement on line $2$. The peeled
statements on lines $6$ and $13$ are within the scope of the conditional
branch statement on line $2$. Thus, $\mathsf{CondNodes}$ = { $2$ } and
$\mathit{Locs}$ = { $2b$, $5$, $6b$, $9$, $10b$, $12$ }. The program
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ is the program fragment consisting of
the nodes in the set $\mathit{Locs}$ in Tab. 1(d). Notice that the non-peeled
conditional branch node in $\mathsf{P}_{N}^{p}$ (on line $2$) that has the
peeled nodes within its scope is retained in
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ along with the peels of loops.

######  Lemma 17.

Let $\mathsf{P}_{N}^{p}$ be a peeled program and let $vA$ be a scalar
variable/array in $\mathsf{P}_{N}^{p}$ that is absent in
$\mathsf{AffectedVars}$ when ComputeAffected is executed on
$\mathsf{P}_{N}^{p}$. If $\mathsf{P}_{N}^{o}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ are executed from the same
state $\sigma$, then $vA$ has the same value on termination of both programs.

Proof: We break the proof in two parts. We first show that if
$\mathsf{P}_{N}^{o}$ and $\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ are executed starting from
the same state $\sigma$, then $vA$ has the same value on termination of both
programs. This follows easily from Lemmas 13, 15 and 16.

Next we show that if $\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ and
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$
are executed from the same state $\sigma$, then $vA$ has the same value on
termination of both programs. We prove this part by case analysis.

Suppose the last update to $vA$ in $\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ happens in a non-peeled node
in $\mathsf{P}_{{N}}^{\star}$. Then, the proof follows immediately from Lemma
11.

Suppose the last update to $vA$ in $\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ happens in a peeled node $n$
in $\mathsf{Peel}({\mathsf{P}_{N}^{p}})$. Let $S$ denote the set of
variables/arrays $vA^{\prime}$ such that the updated value of $vA$ at node $n$
depends on the values of each $vA^{\prime}\in S$ on termination of
$\mathsf{P}_{{N}}^{\star}$. There are two sub-cases to consider.

If no $vA^{\prime}\in S$ is identified as affected by ComputeAffected, then by
Lemma 11 the value of every such $vA^{\prime}$ is the same after termination
of $\mathsf{P}_{{N}}^{\star}$ and $\mathsf{P}_{N-1}$. This implies that the
value of $vA$ is also same after termination of
$\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ and
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$.

Now consider the case where some $vA^{\prime}\in S$ is identified as affected
by ComputeAffected. Let $L$ be a loop in $\mathsf{P}_{N}^{p}$ from which the
node $n$ is peeled. From the construction of peeled nodes, we know that for
every node $n$ in the peel of $L$ there is a corresponding node $n^{\prime}$
in the “uncollapsed” body of loop $L$ such that the $\mathit{def}$ and
$\mathit{uses}$ sets of the two nodes $n$ and $n^{\prime}$ coincide. Since the
update to $vA$ at node $n$ depends on $vA^{\prime}$ that is identified as
affected, the update to $vA$ at node $n^{\prime}$ in loop $L$ must also depend
on the affected variable/array $vA^{\prime}$. However, this would cause
ComputeAffected to identify $vA$ as an affected variable. This leads to a
contradiction since we know $vA$ is not affected. This completes the proof.

Lemma 17 allows us to use $\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ as the
difference program $\partial\mathsf{P}_{N}$ if none of the scalar variables
and arrays of interest are identified as affected by ComputeAffected. This
holds true in the case where the post-condition $\psi^{r}(N)$ does not refer
to any affected variable/array. Note that using
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ as the difference program
$\partial\mathsf{P}_{N}$ works even if there are other variables/arrays (not
of interest) that are affected. However, if some of our variables/arrays of
interest are indeed identified as affected by ComputeAffected, we must include
additional code in the difference program that effectively “rectifies” the
values of affected variables as computed by $\mathsf{P}_{N-1}$. We elaborate
on this in the next subsection.

####  4.5.5 Generalized Computation of Difference Programs

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = 0;
    2.  for(i=0; i<N-1; i++) {
    3.    S = S + A[i];
    4.  }

    5.  for(i=0; i<N-1; i++) {
    6.    A1[i] = A[i] + S;
    7.  }

    8.  S1 = S;
    9.  for(i=0; i<N-1; i++) {
    10.   S1 = S1 + A1[i];
    11. }

    12. S = S + A[N-1];
    13. A1[N-1] = A[N-1] + S;
    14. S1 = S1 + A1[N-1];

    // assert(S1 = N

    $\ignorespaces\times$

     (N+2))

Figure 21: Hoare triple with the program $\mathsf{P}_{N-1}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}})$

Recall that $\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ was constructed by replacing
some of the nodes in the collapsed CFG of $\mathsf{P}_{N}^{p}$ with
$\mathsf{skip}$ and by simplifying the resulting CFG. As seen above, this
suffices to serve as the difference program $\partial\mathsf{P}_{N}$ if none
of the variables/arrays of interest are identified as affected by function
ComputeAffected. If, however, some variables/arrays of interest are identified
as affected, $\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ as computed above may no
longer serve as a correct difference program. To see an example of this,
consider the peeled program in Fig. 17. If we were to compute
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ for this program we would get the
program fragment in lines $12-14$ shown in Fig. 21. In this program, array A1
and scalar variable S1 are identified as affected. Notice that, the program
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}})$ in
Fig. 21 computes incorrect values of A1 at line $6$ and S1 at line $14$.

Interestingly, even in cases like the above example, a correct difference
program can often be constructed by modifying the way in which
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$ is constructed. To prevent confusion, we
do not call the program resulting from this modified construction as
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$. Instead we call it
$\partial\mathsf{P}_{N}$. The modification referred to above concerns which
statements are replaced by $\mathsf{skip}$ and which are retained but possibly
with a change. Specifically, all assignment statements that update an affected
variable/array but were earlier (while constructing
$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$) replaced by $\mathsf{skip}$ are
retained with a possibly changed expression in the right hand side of the
assignment. Since no new nodes are added to the CFG of $\mathsf{P}_{N}$ in
this way of constructing $\partial\mathsf{P}_{N}$, there is a natural
injective mapping, say $\beta$, from the nodes in the CFG of
$\partial\mathsf{P}_{N}$ to those in the CFG of $\mathsf{P}_{N}$.

To understand how the right hand side expressions of assignments may need to
be changed when constructing $\partial\mathsf{P}_{N}$, consider an execution
of each of $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ starting from the same initial state
$\sigma$.

######  Definition 1.

For every node $n$ in the CFG of $\partial\mathsf{P}_{N}$ and for every
variable/array element $vA$ we say that $vA$ has a _rectified value_ at $n$ if
its value at $n$ matches the value of $vA$ at $\beta(n)$. Otherwise, we say
that $vA$ has an _unrectified value_ at $n$.

For every node $n$ in $\partial\mathsf{P}_{N}$ that updates an affected
variable/array $vA$ of interest, we modify the right hand side of the
assignment (if necessary) such that the right hand side expression evaluates
to the rectified value of $vA$ at $n$. This expression is constructed in such
a manner that it uses the unrectified value of $vA$ at $n$ (if the assignment
statement was replaced by a $\mathsf{skip}$) in its computation of the
rectified value. This construction allows us to establish an important
property of the resulting program $\partial\mathsf{P}_{N}$: every
variable/array $vA$ of interest has its rectified value at every node $n$ in
$\partial\mathsf{P}_{N}$.

We now elaborate on how we construct the modified right hand side expression
of an assignment statement at node $n$ in $\partial\mathsf{P}_{N}$ that
updates the affected variable/array $vA$. We assume that we have access to the
rectified and unrectified values of all variables/arrays $vA^{\prime}$ used in
the right hand side expression of the assignment statement at node $\beta(n)$
in $\mathsf{P}_{N}$. The easiest way to do this would be to construct the
right hand side expression exclusively in terms of the rectified values of
$vA^{\prime}$ at node $n$. Note that, this results in a difference program
that is as complex as the original program $\mathsf{P}_{N}$. This defeats our
purpose, since full-program induction can succeed only if
$\partial\mathsf{P}_{N}$ is “simpler” than $\mathsf{P}_{N}$. Therefore, we do
not use this naive method and present an operator algebra to compute of the
rectified value of $vA$ updated in the assignment statement in terms of its
unrectified value and the “difference” between the rectified and unrectified
values of other variables/arrays that have a data dependence to $vA$.

Let $\circ$ be a binary operator on a set $\mathcal{S}$ that denotes the
domain of values of variables/arrays in $\mathsf{P}_{N}$. We say that $e$ is
the right identity element of $\circ$ if $v$ $\circ$ $e$ = $v$ and $e$ is the
left identity element if $e$ $\circ$ $v$ = $v$ for each $v\in\mathcal{S}$. We
call $v^{-\circ}$ the right inverse element of $v$ under $\circ$ if $v$
$\circ$ $v^{-\circ}$ = $e$ and we call it the left inverse element if
$v^{-\circ}$ $\circ$ $v$ = $e$ for each $v\in\mathcal{S}$. We say that $\circ$
is an associative operator if $(u\circ v)\circ w$ = $u\circ(v\circ w)$. We say
that $\circ$ is a commutative operator if $u\circ v$ = $v\circ u$. When the
operator $\circ$ is associative, $(u\circ v)^{-\circ}$ = $(v^{-\circ}\circ
u^{-\circ})$.

For the following lemmas, we assume that $\circ$ is an associative operator,
there exists a left identity element under $\circ$ in $\mathcal{S}$ and each
element in $\mathcal{S}$ has a right inverse under $\circ$.

######  Lemma 18.

Let $n$ be a node in $\partial\mathsf{P}_{N}$ such that the statement at
$\beta(n)$ in $\mathsf{P}_{N}$ is $w$ $:=$ $u$ $\circ$ $v$. Suppose $w$ is an
affected variable/array of interest. Let $w_{N-1}$, $u_{N-1}$, $v_{N-1}$
denote the values of $w$, $u$ and $v$ at the end of execution of
$\mathsf{P}_{N-1}$. Let $w_{N}$, $u_{N}$, $v_{N}$ be the rectified values of
$w$, $u$ and $v$ at node $n$. Then the rectified value of $w$ is computed as
$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((v_{N-1})^{-\circ}$ $\circ$
$((u_{N-1})^{-\circ}$ $\circ$ $u_{N})$ $\circ$ $v_{N})$.

Proof: We proceed as follows:

  1. 1.

$w_{N}$ $:=$ $e$ $\circ$ $w_{N}$

  2. 2.

$w_{N}$ $:=$ $(w_{N-1}$ $\circ$ $(w_{N-1})^{-\circ})$ $\circ$ $w_{N}$

  3. 3.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((w_{N-1})^{-\circ}$ $\circ$ $w_{N})$

  4. 4.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((u_{N-1}$ $\circ$ $v_{N-1})^{-\circ}$ $\circ$
$(u_{N}$ $\circ$ $v_{N}))$

  5. 5.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((v_{N-1})^{-\circ}$ $\circ$
$(u_{N-1})^{-\circ}$ $\circ$ $(u_{N}$ $\circ$ $v_{N}))$

  6. 6.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((v_{N-1})^{-\circ}$ $\circ$
$((u_{N-1})^{-\circ}$ $\circ$ $u_{N})$ $\circ$ $v_{N})$

Suppose $\circ$ is additionally a commutative operator. Then the following
lemmas hold.

######  Lemma 19.

Under the assumptions stated in Lemma 18, the rectified value of $w$ is
computed as $w_{N}$ := $w_{N-1}$ $\circ$ $(u_{N}$ $\circ$
$(u_{N-1})^{-\circ})$ $\circ$ $(v_{N}$ $\circ$ $(v_{N-1})^{-\circ})$.

Proof: We continue from the proof of Lemma 18 and proceed as follows:

  1. 6.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((v_{N-1})^{-\circ}$ $\circ$
$((u_{N-1})^{-\circ}$ $\circ$ $u_{N})$ $\circ$ $v_{N})$

  2. 7.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $(((u_{N-1})^{-\circ}$ $\circ$ $u_{N})$ $\circ$
$(v_{N-1})^{-\circ}$ $\circ$ $v_{N})$

  3. 8.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $((u_{N-1})^{-\circ}$ $\circ$ $u_{N})$ $\circ$
$((v_{N-1})^{-\circ}$ $\circ$ $v_{N})$

  4. 9.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $(u_{N}$ $\circ$ $(u_{N-1})^{-\circ})$ $\circ$
$(v_{N}$ $\circ$ $(v_{N-1})^{-\circ})$

To use the equation from Lemma 19 for statements with non-commutative
operators such as $\\{-,\div\\}$ often used in practice, we perform a simple
transformation that allows us to use commutative operators inplace of non-
commutative ones. As an example of this transformation, consider the
expressions $u-v$ and $u/v$. We transform them into the expressions $u+(-v)$
and $u\times(1/v)$ respectively. This allows us to use the equation in Lemma
19 when for every element $v\in\mathcal{S}$, the elements $-v$ and $1/v$ are
also in $\mathcal{S}$.

######  Lemma 20.

Let $n$ be a node in $\partial\mathsf{P}_{N}$ such that the statement at
$\beta(n)$ in $\mathsf{P}_{N}$ is $w$ $:=$ $w$ $\circ$ $v$. Then the rectified
value of $w$ is computed as $w_{N}$ := $w_{N}$ $\circ$ $(v_{N}$ $\circ$
$(v_{N-1})^{-\circ})$ along with the presumption $w_{N}=w_{N-1}$.

Proof: Using the given presumption $w_{N}=w_{N-1}$, we have the definition of
the identity element as: $e$ $=$ $w_{N}\circ(w_{N})^{-\circ}$ $=$
$w_{N}\circ(w_{N-1})^{-\circ}$.

As the first step, we use the result from Lemma 19 and proceed as follows:

  1. 1.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $(w_{N}$ $\circ$ $(w_{N-1})^{-\circ})$ $\circ$
$(v_{N}$ $\circ$ $(v_{N-1})^{-\circ})$

  2. 2.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $e$ $\circ$ $(v_{N}$ $\circ$
$(v_{N-1})^{-\circ})$

  3. 3.

$w_{N}$ $:=$ $w_{N-1}$ $\circ$ $(v_{N}$ $\circ$ $(v_{N-1})^{-\circ})$

  4. 4.

$w_{N}$ $:=$ $w_{N}$ $\circ$ $(v_{N}$ $\circ$ $(v_{N-1})^{-\circ})$

It is worth noting that the rectification described in Lemmas 18, 19 and 20
applies not only when the set $\mathcal{S}$ is integers, i.e. integers are
stored as array elements but even when the set consists of matrices, vectors,
and polynomials. When matrices are stored as array elements, such arrays are
called tensors. These are extensively used in machine learning algorithms.
Further, it applies to interesting operators such as $\boldsymbol{\oplus}$,
$\boldsymbol{+}$ $mod$ $x$, $\boldsymbol{\times}$ $mod$ $y$ as well as to
other interesting algebraic structures. It is also worth mentioning that for a
restricted class of programs our technique extends to computing the
differences of programs that manipulate heaps.

Algorithm 4 ProgramDiff($(\mathit{Locs},CE,\mu)$: renamed program
$\mathsf{P}_{N}$, $\mathsf{GlueNodes}$: set of glue nodes)

1:$\langle(\mathit{Locs}^{p},CE^{p},\mu^{p}),\mathsf{PeelNodes}\rangle$ :=
PeelAllLoops($(\mathit{Locs},CE,\mu)$);

2:$\mathsf{AffectedVars}$ :=
ComputeAffected$((\mathit{Locs}^{p},CE^{p},\mu^{p}),\mathsf{PeelNodes})$;

3:$\partial\mathsf{P}_{N}:=(Locs^{\prime},CE^{\prime},\mu^{\prime})$, where
$Locs^{\prime}:=Locs^{p}$, $CE^{\prime}:=CE^{p}$, and $\mu^{\prime}:=\mu^{p}$;

4:$\partial\mathsf{P}_{N}:=\textsc{CollapseLoopBody}(\partial\mathsf{P}_{N})$;
$\ignorespaces\triangleright$ Collapse nodes and edges of each loop into its
loop-head

5:$\mathsf{WorkList}$ := $(n_{start})$;  $\ignorespaces\triangleright$ Add the
start node to the worklist

6:$\mathsf{ProcessedNodes}$ := $\emptyset$;

7:while $\mathsf{WorkList}$ is not empty do

8: Remove a node $n$ from head of $\mathsf{WorkList}$;

9: $\mathsf{ProcessedNodes}$ := $\mathsf{ProcessedNodes}\cup\\{n\\}$;

10: for each node $n^{\prime}\in$ Succ$(n)\setminus\mathsf{ProcessedNodes}$ do

11: $\mathsf{WorkList}$ := AppendToList($\mathsf{WorkList}$, $n^{\prime}$);

12: end for

13: if $n\in\mathsf{PeelNodes}$ then continue;  $\ignorespaces\triangleright$
Difference computation not required

14: else if HasAffectedVars($n$, $\mathsf{AffectedVars}$) then

15: if $n\in\mathsf{GlueNodes}$ then continue;  $\ignorespaces\triangleright$
Retain the glue loop

16: else if $n$ is a loop-head then

17: $L:=\textsc{UncollapseLoopBody}(n)$;  $\ignorespaces\triangleright$
Uncollapse the loop-head

18: for each node $n^{\prime}\in\textsc{Nodes}(L)$ do

19: if HasAffectedVars($n^{\prime}$, $\mathsf{AffectedVars}$) then

20:
$\mu^{\prime}(n^{\prime}):=\textsc{NodeDiff}(n^{\prime},\mu,\mathsf{AffectedVars})$;

21: else $\partial\mathsf{P}_{N}$ := RemoveNode($n^{\prime}$,
$\partial\mathsf{P}_{N}$);  $\ignorespaces\triangleright$ No affected
variables at node $n^{\prime}$

22: end if

23: end for

24: else $\mu^{\prime}(n):=\textsc{NodeDiff}(n,\mu,\mathsf{AffectedVars})$;

25: end if

26: else $\ignorespaces\triangleright$ No affected variables at node $n$

27: Let $\mathsf{CondNodes}$ be the set of all branch nodes that have a peeled
node within its scope;

28: if $n\not\in\mathsf{CondNodes}$ then $\partial\mathsf{P}_{N}$ :=
RemoveNode($n$, $\partial\mathsf{P}_{N}$);

29: end if

30: end if

31:end while

32:return ${\partial\mathsf{P}_{N}}$;

HasAffectedVars( $n$: node, $\mathsf{AffectedVars}$: set of affected variables
)

1:if $\exists vA$ such that $vA\in\mathit{def}(n)$ and
$vA\in\mathsf{AffectedVars}$ then return $\mathsf{True}$;

2:else return $\mathsf{False}$;

3:end if

NodeDiff( $n$: node, $\mu$: node labelling function, $\mathsf{AffectedVars}$:
set of affected variables )

1:if $\mu(n)$ is of the form $w_{N}:=r^{1}_{N}$ op $r^{2}_{N}$ then

2: return $w_{N}$ $:=$ $w_{N-1}$ $\circ$ $(r^{1}_{N}$ $\circ$
$(r^{1}_{N-1})^{-\circ})$ $\circ$ $(r^{2}_{N}$ $\circ$
$(r^{2}_{N-1})^{-\circ})$;  $\ignorespaces\triangleright$ Refer Lemma 19

3:else if $\mu(n)$ is of the form $w_{N}:=w_{N}$ op $r^{1}_{N}$ wherein
$w_{N}$ is a scalar then

4: return $w_{N}$ $:=$ $w_{N}$ $\circ$ $(r^{1}_{N}$ $\circ$
$(r^{1}_{N-1})^{-\circ})$;  $\ignorespaces\triangleright$ Refer Lemma 20

5:else $\ignorespaces\triangleright$ $\mu(n)$ is a conditional statement
$C_{N}$

6: if ($\exists v$ s.t. $v\in uses(n)$ and $v\in\mathsf{AffectedVars}$) $\vee$
($C_{N}\not=C_{N-1}$ is satisfiable) then

7: throw “Branch conditions in $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$ may not
evaluate to same value”;

8: else return $\mu(n)$;

9: end if

10:end if

The routine ProgramDiff presented in Algorithm 4 shows how the difference
program is computed. In line 1, we peel each loop in the program
$\mathsf{P}_{N}$ and collect the list of peeled nodes using Algorithm 1. We
then compute the set of affected variables using Algorithm 3 (line 2). The
difference program $\partial\mathsf{P}_{N}$ inherits the skeletal structure of
the peeled program $\mathsf{P}^{p}_{N}$ after peeling each loop (line 3).
Next, we collapse all nodes and edges in the body of each loop into a single
node identified with the loop-head in the CFG of $\mathsf{P}^{p}_{N}$ using
the function CollapseLoopBody in line 4. The collapsed CFG of the resulting
program $\partial\mathsf{P}_{N}$ is a DAG with finitely many paths. We then
initialize a worklist of CFG nodes with $n_{start}$ in line 5.

The while loop in lines 7–31 performs a breadth-first top-down traversal over
the DAG of $\partial\mathsf{P}_{N}$ starting from the node $n_{start}$ and
processes one node at a time. We first remove a node $n$ from the worklist in
line 8. We store the nodes that are already processed by our algorithm in
$\mathsf{ProcessedNodes}$ (that is initialized in line 6). We add the node $n$
removed from the worklist to $\mathsf{ProcessedNodes}$ in line 9. Next, the
loop in lines 10–12 appends each successor $n^{\prime}$ of $n$ to the worklist
that is not already processed. We use the routine Succ to obtain the list of
successors of node $n$.

If $n$ is a peeled node, then we retain it as is in the difference program
(line 13). Otherwise, we check if any scalar variable/array used at node $n$
is affected at line 14. We have defined the sub-routine HasAffectedVars that
checks if the scalar variable/array defined at node $n$ is affected.

For nodes $n$ that refer to an affected variable/array, we do the following.
We check if a node $n$ is a glue node that refers to an affected
variable/array in line 15 and retain such nodes as is in the difference
program. Otherwise, we check if the node $n$ corresponds to a loop-head in
line 16. We uncollapse the nodes corresponding to a loop-head that represent
the entire loop in line 17. We assume that the sub-routine Nodes($L$) returns
the set of CFG nodes in loop $L$. Next, the loop in lines 18–23 iterates over
all nodes $n^{\prime}$ in the body of $L$ and process one node at a time. In
line 19, we check if the variable/array updated at node $n^{\prime}$ is
affected using function HasAffectedVars, and compute its rectified value in
line 20, using the function NodeDiff. If the variable/array defined at
$n^{\prime}$ is not identified as affected, then we remove from
${\partial\mathsf{P}_{N}}$ nodes $n^{\prime}$ that do not update an affected
variable/array using the routine RemoveNode in line 21. For a non-peeled node
$n$ that does not correspond to a loop-head, we compute the rectified value of
an affected variable/array defined at $n$ in line 24, using the function
NodeDiff.

For nodes $n$ that are not peeled nodes and do not update an affected
variable/array, we do the following. We compute the set $\mathsf{CondNodes}$
of conditional branch nodes that have at least one peeled node within its
scope in line 27. In line 28, we remove from ${\partial\mathsf{P}_{N}}$ nodes
$n$ (including collapsed loop nodes) that do not update an affected
variable/array and are not in the set $\mathsf{CondNodes}$, using the routine
RemoveNode, as they do not need any rectification.

The sub-routine NodeDiff computes the statements that rectify values of
variables/arrays updated at a node. It determines the type of statement
(assignment, aggregation or branch condition) at the given node and acts
accordingly. For assignment statements, we compute the rectified value as
shown in Lemma 19 and for aggregating statements, we compute the rectified
value as shown in Lemma 20. For the nodes representing a conditional branch in
$\partial\mathsf{P}_{N}$, we determine if its conditional expression evaluates
to the same value in $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$. If so, the
conditional branch is retained as is in $\partial\mathsf{P}_{N}$. Otherwise,
currently our technique cannot compute ${\partial\mathsf{P}_{N}}$ and we
report a failure using the throw statement.

To explain the intuition behind the steps of Algorithm 4, we use the
convention that all variables and arrays of $\mathsf{P}_{N-1}$ have the suffix
_Nm1 (for N-minus-1), while those of $\mathsf{P}_{N}$ have the suffix _N. This
allows us to express variables/arrays of $\mathsf{P}_{N}$ in terms of the
corresponding variables/arrays of $\mathsf{P}_{N-1}$ in a systematic way in
${\partial\mathsf{P}_{N}}$, given that the intended composition is
$\mathsf{P}_{N-1}\mathchar 24635\relax\;{\partial\mathsf{P}_{N}}$.

For assignment statements, we compute the rectified values as follows. For
every assignment statement of the form v = E; in $L$, a corresponding
statement is generated in ${\partial\mathsf{P}_{N}}$ that expresses v_N in
terms of v_Nm1 and the difference (or ratio) between versions of
variables/arrays that appear as sub-expressions in E in $\mathsf{P}_{N-1}$ and
$\mathsf{P}_{N}$.

While the implementation is currently restricted to simple arithmetic
operators ($+,-,\times,\div$), specifically for the ease of implementation and
its use in practice, as previously stated, our rectification method is general
and applies to several operators beyond the ones mentioned here. The following
example shows the computation of rectified values of variables/arrays updated
in simple program statements.

######  Example 10.

The statement A_N[i] = B_N[i] + v_N; in $\mathsf{P}_{N}$ gives rise to the
statement A_N[i] = A_Nm1[i] + (B_N[i] + (- B_Nm1[i])) \+ (v_N + (- v_Nm1)); in
${\partial\mathsf{P}_{N}}$ that rectifies the value of A_N[i]. Similarly, the
statement A_N[i] = B_N[i] * v_N; in $\mathsf{P}_{N}$ gives rise to the
statement A_N[i] = A_Nm1[i] * (B_N[i] * (1/B_Nm1[i])) * (v_N * (1/v_Nm1));
under the assumption B_Nm1[i] * v_Nm1 $\neq 0$.

The program ${\mathsf{P}_{N}}$ may have statements that aggregate/accumulate
values in scalars. This kind of statement requires special processing when
generating the difference program ${\partial\mathsf{P}_{N}}$. The next example
shows the computation of rectified values of variables/arrays in statements
that accumulate values in scalar variables.

######  Example 11.

Consider the loop for(i=0; i<N; i++) { sum_N = sum_N + A_N[i]; }  in program
$\mathsf{P}_{N}$. The difference A_N[i] + (- A_Nm1[i]) is aggregated over all
indices from $0$ through $N-2$. In this case, the loop in
${\partial\mathsf{P}_{N}}$ that rectifies the value of sum_N has the following
form: sum_N = sum_Nm1; for (i=0; i<N-1; i++) { sum_N = sum_N + (A_N[i] + (-
A_Nm1[i])); }. A similar aggregation for multiplicative ratios can also be
shown.

Conditional branch statements pose a considerable challenge to the computation
of difference programs. A branch condition may evaluate to different outcomes
in $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$, for the same value of $N$. When
this happens, programs $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$ execute totally
unrelated blocks of statements. In such situations, it is immensely difficult
to rectify the values of variables/arrays computed along the unrelated
branches, and hence, our algorithm avoids doing so. Only when we can determine
that the condition evaluates to the same value in $\mathsf{P}_{N}$ and
$\mathsf{P}_{N-1}$, we rectify values of variables/arrays computed along the
corresponding branches. Next we present examples with branch conditions to
highlight this.

######  Example 12.

Consider the conditional branch statement if(t3 == 0)  in line $10$ of Fig. 1.
The branch condition evaluates to the same value in $\mathsf{P}_{N}$ and
$\mathsf{P}_{N-1}$ because the condition has no dependence on $N$. Therefore,
the branch statement is used as is during the computation of the difference
program. However, recall that since the arrays accessed in the program are not
affected, none of the loops are retained in the difference program shown in
Fig. 3.

Consider another conditional branch statement if(A[i] == N) in
$\mathsf{P}_{N}$. The corresponding statement in $\mathsf{P}_{N-1}$ is if(A[i]
== N-1). Clearly, the conditions in these statements do not evaluate to the
same value in $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$. Thus, our algorithm
flags a failure to compute the difference program and terminates.

    x = N;
    y = N;
    for(i=0; i<N; i++) {
      if(x == y)
        A[i] = i;
    }

(a)

    x = N-1;
    y = N-1;
    for(i=0; i<N-1; i++) {
      if(x == y)
        A[i] = i;
    }

(b)

Figure 22: Example program (a) $\mathsf{P}_{N}$ and (b) $\mathsf{P}_{N-1}$

There are programs where conditional branch statements with dependence on $N$
evaluate to the same value. For example, consider the program $\mathsf{P}_{N}$
in Fig. 22(a). The program $\mathsf{P}_{N-1}$ is shown in Fig. 22(b). While
the branch condition (indirectly) depends on the value of $N$, it evaluates to
the same value in $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$, since the amount of
change in the value of variables x and y used in the branch condition is same.
Our algorithm can successfully compute the difference program in such cases.

The restriction on branch conditions that use affected variables/arrays can be
further relaxed by handling the case when the condition evaluates to
$\mathsf{True}$ in $\mathsf{P}_{N-1}$ and to $\mathsf{False}$ in
$\mathsf{P}_{N}$ by restoring the values of variables/arrays to their values
at the predecessor of the branch node. However, when a branch condition
evaluates to $\mathsf{False}$ in $\mathsf{P}_{N-1}$ and to $\mathsf{True}$ in
$\mathsf{P}_{N}$, the entire computation within the branch has to be performed
again in $\partial\mathsf{P}_{N}$ instead of just executing the rectification
code. For example, consider the branch statement, if(i < N) Loop;. If the
branch condition i $<$ N-1 in $\mathsf{P}_{N-1}$ evaluates to
$\mathsf{False}$, then the condition i $<$ N in $\mathsf{P}_{N}$ definitely
evaluates to $\mathsf{True}$. This will require the difference program to
execute the entire computation performed by the code fragment Loop; and not
just the difference program corresponding to Loop;. This will hamper the
progress guarantees on the class of programs that our technique can verify.
Hence, we currently avoid handling these cases in the algorithms and consider
them as a part of future work.

We now prove the soundness of the routine ProgramDiff from Algorithm 4. For
the following lemma, we assume that $\partial\mathsf{P}_{N}$ is the difference
program computed when function ProgramDiff is invoked on the renamed program
$\mathsf{P}_{N}$. Suppose both $\mathsf{P}_{N}^{p}$ and
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\partial\mathsf{P}_{N}$ are executed
from the same initial state $\sigma$. We assume
$\pi:(n_{0},n_{1},\ldots,n_{k})$ to be the path in the CFG of
$\partial\mathsf{P}_{N}$ corresponding to the execution of the difference
program from the state obtained after $\mathsf{P}_{N-1}$ has terminated (in
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\partial\mathsf{P}_{N}$). We assume
$\pi^{\prime}:(n_{0}^{\prime},n_{1}^{\prime},\ldots,n_{k}^{\prime})$ to be the
corresponding path in the CFG of the peeled program $\mathsf{P}^{p}_{N}$.

######  Lemma 21.

For every node $n_{j}$ in $\pi$, the rectified values of all variables/array
elements used at $n_{j}$ during the execution of $\partial\mathsf{P}_{N}$ are
identical to the values of the same variables/array elements at the
corresponding node $n^{\prime}_{j}$ during the execution of
$\mathsf{P}^{p}_{N}$.

Proof: If $vA$ is not identified as an affected variable/array by function
ComputeAffected, the result follows from the proof of Lemma 17 and the no-
overwriting property of renaming.

If $vA$ is identified as an affected variable, we induct on the length of
$\pi$. The only difference in this case is that we also need to consider the
assignment statements modified by function NodeDiff at lines 20 and 24 of
function ProgramDiff. Lemmas 18, 19 and 20 guarantee the correctness of the
rectified value of $vA$ computed by these additional statements, given the
unrectified value of $vA$ and rectified and unrectified values of all
variables and array elements used in the right hand side of the assignment. By
the inductive hypothesis, the rectified values of the latter set of variables
and array elements are indeed available. By the no-overwriting property, the
unrectified values of $vA$ and all other variables and arrays used in the
right hand side of the assignment are also available. Therefore, the correct
rectified value of $vA$ is computed at each node in $\pi$.

Finally, note that once a rectified value is generated at a non-glue node in
the difference program, renaming ensures that it is not re-defined by
subsequent statements in the difference program. Therefore, rectified values,
once computed in the difference program, are available for use at subsequent
nodes in the execution path. Putting the above parts together completes the
proof.

######  Theorem 2.

$\partial\mathsf{P}_{N}$ generated by ProgramDiff is such that, for all $N>1$,
$\\{\varphi(N)\\}\;\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}\;\\{\psi(N)\\}$ holds iff
$\\{\varphi(N)\\}\;\mathsf{P}_{N}\;\\{\psi(N)\\}$ holds.

Proof: Lemma 6 guarantees that
$\\{\varphi(N)\\}\;\mathsf{P}_{N}\;\\{\psi(N)\\}$ holds iff
$\\{\varphi(N)\\}\;\mathsf{P}_{N}^{p}\;\\{\psi(N)\\}$ holds. Furthermore,
Lemma 21 ensures that for every state $\sigma$ satisfying $\varphi(N)$, if we
execute $\mathsf{P}_{N}^{p}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ starting from $\sigma$, then if the final
state after termination of $\mathsf{P}_{N}^{p}$ satisfies $\psi(N)$, so does
the final state after termination of $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$. This proves the theorem.

######  Example 13.

We illustrate the difference computation performed by the routine ProgramDiff
in Algorithm 4 on our running example. Fig. 23 shows the difference program
obtained after executing the algorithm on the program in Fig. 17. Notice that
while some program statements in Fig. 23 are syntactically similar to
corresponding statements in Fig. 17, the additional statements (e.g. at lines
3, 6 and 8) in Fig. 23 have no syntactic counterpart in Fig. 17. For the first
loop, since variable S is not affected, only the peeled iteration is retained.
Since A1 and S1 both are affected, the statements in the second and the third
loop are replaced with statements that rectify their values, along with
inserting the peeled statements for both loops. Initialization of variable S1
is also replaced with the statement that rectifies its value since it depends
on the value of S computed in a peel.

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = S_Nm1 + A[N-1];

    2.  for(i=0; i<N-1; i++) {
    3.    A1[i] = A1_Nm1[i] + (S - S_Nm1);
    4.  }
    5.  A1[N-1] = A[N-1] + S;

    6.  S1 = S1_Nm1 + (S - S_Nm1);
    7.  for(i=0; i<N-1; i++) {
    8.    S1 = S1 + (A1[i] - A1_Nm1[i]);
    9.  }
    10. S1 = S1 + A1[N-1];

    // assert(S1 = N

    $\ignorespaces\times$

     (N+2))

Figure 23: Hoare triple with the difference program

###  4.6 Simplifying the Difference Program

Algorithm 5 SimplifyDiff($(\mathit{Locs},CE,\mu)$: difference program
$\partial\mathsf{P}_{N}$)

1:$\partial\mathsf{P}^{\prime}_{N}:=(Locs^{\prime},CE^{\prime},\mu^{\prime})$,
where $Locs^{\prime}:=Locs$, $CE^{\prime}:=CE$, and $\mu^{\prime}:=\mu$;

2:for each loop $L\in\textsc{Loops}(\partial\mathsf{P}^{\prime}_{N})$ do

3: for each node $m\in\textsc{Nodes}(L)$ do

4: $\mu^{\prime}(m)$ := Simplify($\mu^{\prime}(m)$);
$\ignorespaces\triangleright$ Simplify the statement

5: end for

6: $(n_{1},n,c):=\textsc{IncomingEdge}(L)$;  $\ignorespaces\triangleright$ $c$
is the label of the edge from $n_{1}$ to $n$

7: $(n,n_{2},\mathbf{ff}):=\textsc{ExitEdge}(L)$;

8: if body of $L$ is of the form $w_{N}:=w_{N}$ op $expr$, wherein $w_{N}$ is
a scalar variable then

9: $n_{acc}$ = $\textsc{FreshNode}()$;

10: if op $\in\\{+,-\\}$ then

11: $\mu^{\prime}(n_{acc})$ := ($w_{N}:=w_{N}$ op Simplify$(k_{L}(N-1)\times
expr)$);  $\ignorespaces\triangleright$ Accelerated statement

12: else if op $\in\\{\times,\div\\}$ then

13: $\mu^{\prime}(n_{acc})$ := ($w_{N}:=w_{N}$ op
Simplify$(expr^{k_{L}(N-1)})$);  $\ignorespaces\triangleright$ Accelerated
statement

14: else

15: throw “Specified operator not handled”;

16: end if

17: $CE^{\prime}:=CE^{\prime}$ $\cup$
$\\{(n_{1},n_{acc},c),(n_{acc},n_{2},\mathsf{U})\\}$ $\setminus$
$\\{(n_{1},n,c),(n,n_{2},\mathbf{ff})\\}$;

18: $Locs^{\prime}$ := $Locs^{\prime}$ $\cup$ $\\{n_{acc}\\}$ $\setminus$
$\textsc{Nodes}(L)$;

19: end if

20: if body of $L$ is of the form $w_{N}:=w_{N-1}$ or $w_{N}:=w_{N}$ then
$\ignorespaces\triangleright$ Remove redundant loops

21: $CE^{\prime}:=CE^{\prime}$ $\cup$ $\\{(n_{1},n_{2},c)\\}$ $\setminus$
$\\{(n_{1},n,c),(n,n_{2},\mathbf{ff})\\}$;

22: $Locs^{\prime}:=Locs^{\prime}$ $\setminus$ $\textsc{Nodes}(L)$;

23: end if

24:end for

25:return $\partial\mathsf{P}^{\prime}_{N}$;

While we have described a simple strategy to generate a difference program
${\partial\mathsf{P}_{N}}$ above, this may lead to unoptimized as well as
redundant statements in the naively generated difference program. Our
implementation aggressively optimizes $\partial\mathsf{P}_{N}$ and removes
redundant code, renaming variables/arrays as needed. The routine SimplifyDiff
in Algorithm 5 simplifies program statements that compute rectified values,
removes redundant loops from the difference program and substitutes loops with
the summarized statements computed using acceleration. This helps in
${\partial\mathsf{P}_{N}}$ having fewer and simpler loops in a lot of cases.
Below, we describe these optimizations and illustrate them using examples.

Since the generation of statements that compute rectified values is not fully
optimized, these statements may have expressions that can be further
simplified using the values computed in other statements in the generated
difference program ${\partial\mathsf{P}_{N}}$. The function Simplify performs
this optimization aggressively and simplifies the statements in the difference
program (lines 3–4 in Algorithm 5). Let us take an example to illustrate the
effect of the Simplify function.

######  Example 14.

Suppose the difference program ${\partial\mathsf{P}_{N}}$ has statements of
the form B_N[i] = B_Nm1[i] + expr1; and v_N = expr2*v_Nm1;. If expr1 and expr2
are constants or functions of $N$ and loop counters, then expressions such as
(B_N[i] - B_Nm1[i]) and (v_N/v_Nm1) can often be simplified from the
statements in the difference program. The expression expr1 is substituted for
B_N[i] - B_Nm1[i] and expr2 for v_N/v_Nm1 respectively.

The difference program ${\partial\mathsf{P}_{N}}$ may contain loops that
perform redundant computation, for example, copying values across versions of
an array corresponding to $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$, due to the
simplification of the statements that compute its rectified value. We remove
such loops from ${\partial\mathsf{P}_{N}}$ in lines 20–23 of Algorithm 5. Let
us illustrate this with an example.

######  Example 15.

Suppose the difference program $\partial\mathsf{P}_{N}$ has the loop for(i=0;
i<N-1; i++) { A_N[i] = A_Nm1[i]; } where A_N is not used subsequently in the
program. Such loops can be removed from the difference program, as these loops
only copy values from the version of array A in $\mathsf{P}_{N-1}$ to its
version in $\mathsf{P}_{N}$, and hence, are redundant.

The difference program ${\partial\mathsf{P}_{N}}$ may also contain loops that
compute values of variables that can be accelerated. We perform this
optimization in lines 8–18 of SimplifyDiff in Algorithm 5. We first check if
the body of a loop $L$ is in the specific form eligible for this optimization
in line 8. If so, we create a fresh node in line 9 to replace $L$. Lines 10–16
of Algorithm 5 label the fresh node with the accelerated statement. If we
encounter operators that are not supported, then we report a failure of our
technique using the throw statement in line 15. Next, we replace the loop with
the fresh node in lines 17–18. We demonstrate this optimization with the
following example.

######  Example 16.

Suppose the difference program has the loop for(i=0; i<N-1; i++) { sum = sum +
1; }. The semantics of the loop can be summarized using the accelerated
statement sum = sum + (N-1);. SimplifyDiff removes this loop from the program
and introduces the accelerated statement instead.

In the following lemma, we use $\partial\mathsf{P}^{\prime}_{N}$ to denote the
program generated by SimplifyDiff.

######  Lemma 22.

$\\{\varphi(N)\\}\;\mathsf{P}_{N-1}\mathchar
24635\relax\;{\partial\mathsf{P}^{\prime}_{N}}\;\\{\psi(N)\\}$ holds iff
$\\{\varphi(N)\\}\;\mathsf{P}_{N-1}\mathchar
24635\relax\;{\partial\mathsf{P}_{N}}\;\\{\psi(N)\\}$ holds.

Proof: Follows trivially from the fact that SimplifyDiff in Algorithm 5
optimizes program statements, removes only redundant statements/loops, and
replaces loops using semantically equivalent accelerated statements.

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = S_Nm1 + A[N-1];

    2.  for(i=0; i<N-1; i++) {
    3.    A1[i] = A1_Nm1[i] + 1;
    4.  }
    5.  A1[N-1] = A[N-1] + S;

    6.  S1 = S1_Nm1 + A[N-1];
    7.  S1 = S1 + (N-1);
    8.  S1 = S1 + A1[N-1];

    // assert(S1 = N

    $\ignorespaces\times$

     (N+2))

Figure 24: Simplification of the difference program

######  Example 17.

We illustrate the application of the simplification routine SimplifyDiff from
Algorithm 5 on our running example. The program in Fig. 24 is obtained after
simplification of $\partial\mathsf{P}_{N}$ in Fig. 23. The difference terms
are replaced with the simplified expressions from the difference program
itself. Notice that the loop that rectifies the value of S1 is accelerated and
the statement obtained after this optimization is shown in line 7.

###  4.7 Generating the Difference Pre-condition $\mathbf{\partial\varphi(N)}$

Algorithm 6 SyntacticDiff($\varphi(N)$: pre-condition)

1:if $\varphi(N)$ is of the form $\forall i\in\\{0\ldots
N\\}\;\widehat{\varphi}(i)$ then

2: if $\varphi(N)\rightarrow\varphi(N-1)$ is invalid then

3: throw “Unable to compute the difference pre-condition";

4: end if

5: ${\partial\varphi(N)}:=\widehat{\varphi}(N)$;

6:else if $\varphi(N)$ is of the form $\exists i\in\\{0\ldots
N\\}\;\widehat{\varphi}(i)$ then

7: if $\varphi(N-1)\rightarrow\varphi(N)$ is invalid then

8: throw “Unable to compute the difference pre-condition";

9: end if

10: ${\partial\varphi(N)}:=\widehat{\varphi}(N)$;

11:else if $\varphi(N)$ is of the form $\varphi^{1}(N)$ $\wedge$ $\cdots$
$\wedge$ $\varphi^{k}(N)$ then

12: ${\partial\varphi(N)}:=$SyntacticDiff($\varphi^{1}(N)$)
$\boldsymbol{\vee}$ $\cdots$ $\boldsymbol{\vee}$
SyntacticDiff($\varphi^{k}(N)$);

13:else if $\varphi(N)$ is of the form $\varphi^{1}(N)$ $\vee$ $\cdots$ $\vee$
$\varphi^{k}(N)$ then

14: ${\partial\varphi(N)}:=$SyntacticDiff($\varphi^{1}(N)$) $\vee$ $\cdots$
$\vee$ SyntacticDiff($\varphi^{k}(N)$);

15:else

16: ${\partial\varphi(N)}:=\mathsf{True}$;

17:end if

18:if $\mathsf{P}_{N-1}$ updates scalars or array elements in
$\partial\varphi(N)$ then

19: ${\partial\varphi(N)}:=\mathsf{True}$;

20:end if

21:return $\partial\varphi(N)$;

We now present a syntactic routine, called SyntacticDiff, in Algorithm 6 for
generation of the difference pre-condition ${\partial\varphi(N)}$. Although
this suffices for all our experiments, for the sake of completeness, we
present later a more sophisticated algorithm for generating
${\partial\varphi(N)}$ simultaneously with $\mathsf{Pre}(N)$ in Sect. 5.3.

Formally, given $\varphi(N)$, the function SyntacticDiff from Algorithm 6
generates a formula ${\partial\varphi(N)}$ such that $\varphi(N)$
$\rightarrow$ $(\varphi(N-1)\odot{\partial\varphi(N)})$, where $\odot$ is
$\wedge$ when $\varphi(N)$ is a universally quantified formula and is $\vee$
when $\varphi(N)$ is a existentially quantified formula. Observe that if such
a ${\partial\varphi(N)}$ exists for universally quantified formulas
$\varphi(N)$, then $\varphi(N)$ $\rightarrow$ $\varphi(N-1)$ must hold.
Similarly, if such a ${\partial\varphi(N)}$ exists for existentially
quantified formulas $\varphi(N)$, then $\varphi(N-1)$ $\rightarrow$
$\varphi(N)$ must hold. Therefore, we can use the validity of $\varphi(N)$
$\rightarrow$ $\varphi(N-1)$ and $\varphi(N-1)$ $\rightarrow$ $\varphi(N)$, as
a test to decide the existence of ${\partial\varphi(N)}$ for universally and
existentially quantified formulas respectively.

Algorithm 6 incorporates the scenarios described above and boolean
combinations thereof. When $\varphi(N)$ is of the syntactic form $\forall
i\in\\{0\ldots N\\}\;\widehat{\varphi}(i)$, we first check the validity of
$\varphi(N)$ $\rightarrow$ $\varphi(N-1)$ in line 2. If this test fails, we
report failure using the throw statement in line 3. Otherwise,
${\partial\varphi(N)}$ is set to $\widehat{\varphi}(N)$ in line 5. Similarly,
when $\varphi(N)$ is of the syntactic form $\exists i\in\\{0\ldots
N\\}\;\widehat{\varphi}(i)$, then ${\partial\varphi(N)}$ is set to
$\widehat{\varphi}(N)$ in line 10, after checking the validity of the
$\varphi(N-1)$ $\rightarrow$ $\varphi(N)$ (line 7). If the test in line 7
fails, again we report failure using the throw statement in line 8. When
$\varphi(N)$ is of the syntactic form $\varphi^{1}(N)$ $\wedge$ $\cdots$
$\wedge$ $\varphi^{k}(N)$, ${\partial\varphi(N)}$ is computed by taking the
difference of each individual conjunct and disjuncting them as
${\partial\varphi^{1}(N)}$ $\vee$ $\cdots$ $\vee$ ${\partial\varphi^{k}(N)}$
(line 12). Note that this operation results in an over-approximation of the
difference pre-condition. When $\varphi(N)$ is of the form $\varphi^{1}(N)$
$\vee$ $\cdots$ $\vee$ $\varphi^{k}(N)$, ${\partial\varphi(N)}$ is computed by
taking the difference of each individual disjunct as
${\partial\varphi^{1}(N)}$ $\vee$ $\cdots$ $\vee$ ${\partial\varphi^{k}(N)}$
(line 14). Finally, if $\varphi(N)$ does not belong to any of these syntactic
forms (line 15) or if condition 2(a) of Theorem 1 is violated by the
${\partial\varphi(N)}$ computed in this manner (line 18), then we over-
approximate ${\partial\varphi_{N}}$ by $\mathsf{True}$ in lines 16 and 19.

######  Lemma 23.

The difference pre-condition $\partial\varphi(N)$ computed by SyntacticDiff is
such that (i) $\varphi(N)$ $\rightarrow$
$(\varphi(N-1)\odot{\partial\varphi(N)})$, where $\odot\in$ {$\wedge$,
$\vee$}, and (ii) $\mathsf{P}_{N-1}$ does not modify variables/arrays in
$\partial\varphi(N)$.

Proof: Condition (i) follows from the checks implemented in lines 2 and 7 of
function SyntacticDiff. The check in line 18 ensures condition (ii). This
concludes the proof.

######  Example 18.

Consider the pre-condition $\varphi(N):=\forall i\in[0,N)\;A[i]=1$ from our
running example in Fig. 24. The difference pre-condition computed by function
SyntacticDiff in Algorithm 6 is $\partial\varphi(N):=A[N-1]=1$ shown by the
assume statement in Fig. 25.

######  Example 19.

Consider the pre-condition $\varphi(N):=\forall i\in[0,N)\;A[i]=1\vee\forall
i\in[0,N)\;A[i]=2$. SyntacticDiff in Algorithm 6 enters the recursive case in
line 14. The recursive invocations with inputs $\varphi_{1}(N):=\forall
i\in[0,N)\;A[i]=1$ and $\varphi_{2}(N):=\forall i\in[0,N)\;A[i]=2$ compute the
difference pre-conditions $\partial\varphi_{1}(N):=A[N-1]=1$ and
$\partial\varphi_{2}(N):=A[N-1]=2$ respectively. On returning from the
recursive case, the algorithm stores the formula $A[N-1]=1\vee A[N-1]=2$ in
$\partial\varphi(N)$.

######  Example 20.

Consider the pre-condition $\varphi(N):=\exists i\in[0,N)\;A[i]\geq 100$
$\wedge$ $\exists j\in[0,N)\;A[j]\leq 10$. The difference pre-condition
computed by function SyntacticDiff in Algorithm 6 is
$\partial\varphi(N):=A[N-1]\geq 100\vee A[N-1]\leq 10$. Notice that the
computed difference pre-condition is an over-approximation. Had we computed
the difference pre-condition as $\partial\varphi(N):=A[N-1]\geq 100\wedge
A[N-1]\leq 10$, then it would have resulted in a contradiction.

######  Example 21.

For pre-condition formulas $\varphi(N)$ := $\forall i\in[0,N)\;$ $A[i]=N$ and
$\varphi(N)$ := $\exists i\in[0,N)\;$ $A[i]=N$ the validity checks at lines 2
and 7 respectively in Algorithm 6 fail. Hence, the algorithm terminates with
out being able to compute an appropriate pre-condition.

##  5 Algorithms for Full-Program Induction

In this section, we discuss the algorithms for full-program induction. The
algorithm primarily focuses on generation of the three crucial components:
_difference program_ ${\partial\mathsf{P}_{N}}$, _difference pre-condition_
${\partial\varphi(N)}$, and the formula $\mathsf{Pre}(N)$ for strengthening
pre- and post-conditions. We have already seen the computation of the
difference program and the difference pre-condition in Sect. 4. Before
describing the algorithm for full-program induction, however, we present the
strategy for computing the formula $\mathsf{Pre}(N)$.

###  5.1 Generating the Formula $\mathbf{\mathsf{Pre}(N-1)}$

We use Dijkstra’s weakest pre-condition computation to obtain
$\mathsf{Pre}(N-1)$ after the difference pre-condition ${\partial\varphi(N)}$
and the difference program ${\partial\mathsf{P}_{N}}$ have been generated. The
weakest pre-condition can always be computed using quantifier elimination
engines in state-of-the-art SMT solvers like Z3 if ${\partial\mathsf{P}_{N}}$
is loop-free. In such cases, we use a set of heuristics to simplify the
calculation of the weakest pre-condition before harnessing the power of the
quantifier elimination engine. If ${\partial\mathsf{P}_{N}}$ contains a loop,
it may still be possible to obtain the weakest pre-condition if the loop
doesn’t affect the post-condition. Otherwise, we compute as much of the
weakest pre-condition as can be computed from the non-loopy parts of
${\partial\mathsf{P}_{N}}$, and then try to recursively solve the problem by
invoking full-program induction on ${\partial\mathsf{P}_{N}}$ with appropriate
pre- and post-conditions.

    // assume(A[N-1] = 1)            //

    $\ignorespaces\partial\varphi$

    (N)
    // assume(S1_Nm1 = (N-1)

    $\ignorespaces\times$

    (N+1)) //

    $\ignorespaces\psi$

    (N-1)
    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N-1) A1_Nm1[i] = N)
    // assume(S_Nm1 = N-1)

    1.  S = S_Nm1 + A[N-1];

    2.  for(i=0; i<N-1; i++) {
    3.    A1[i] = A1_Nm1[i] + 1;
    4.  }
    5.  A1[N-1] = A[N-1] + S;

    6.  S1 = S1_Nm1 + A[N-1];
    7.  S1 = S1 + (N-1);
    8.  S1 = S1 + A1[N-1];

    // assert(S1 = N

    $\ignorespaces\times$

    (N+2))         //

    $\ignorespaces\psi$

    (N)
    // assert(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A1[i] = N+1)
    // assert(S = N)

Figure 25: Strengthening the pre- and post-conditions

######  Example 22.

We apply Dijkstra’s weakest pre-condition computation on the Hoare triple from
our running example in Fig. 24. The Hoare triple in Fig. 25 shows the
difference pre-condition $\partial\varphi(N)$, post-condition $\psi(N)$ and
the formula $\psi(N-1)$ from the induction hypothesis as well as the
strengthened pre- and post-condition formulas. The first application of
weakest pre-condition computation generates the pre-condition A1[N-1] = N+1 on
array A1. This is lifted to the quantified form $\forall i$
$\in[0,\mathtt{N})\;$ $\mathtt{A1}[i]=\mathtt{N}+1$ in a natural way and is
used to strengthen the post-condition. We substitute $N$ with $N-1$ and rename
the array to get the formula $\forall i$ $\in[0,\mathtt{N})\;$
$\mathtt{A1\\_Nm1}[i]=\mathtt{N}$, which is used to strengthen the pre-
condition. Re-applying weakest pre-condition computation generates the
predicates on $\mathtt{S}$ and $\mathtt{S\\_Nm1}$ that further strengthen the
pre- and post-condition as shown in Fig. 25.

###  5.2 Verification by Full-program Induction

Algorithm 7 FPIVerify($\mathsf{P}_{N}$: program, $\varphi(N)$: pre-condition,
$\psi(N)$: post-condition)

1:if Base case check {$\varphi(1)$} $\mathsf{P}_{1}$ {$\psi(1)$} fails then

2: print “Counterexample found!”;

3: return $\mathsf{False}$;

4:end if

5:$\langle\mathsf{P}_{N},\varphi(N),\psi(N),\mathsf{GlueNodes}\rangle$ :=
Rename($\mathsf{P}_{N}$, $\varphi(N)$, $\psi(N)$);
$\ignorespaces\triangleright$ Renaming as described in Sect. 4.1

6:$\partial\varphi(N)$ := SyntacticDiff($\varphi(N)$);

7:$\partial\mathsf{P}_{N}$ := ProgramDiff($\mathsf{P}_{N}$,
$\mathsf{GlueNodes}$);

8:$\partial\mathsf{P}_{N}$ := SimplifyDiff($\partial\mathsf{P}_{N}$);
$\ignorespaces\triangleright$ Simplify and Accelerate loops

9:$i:=0$;

10:$\mathsf{Pre}_{i}(N):=\psi(N)$;

11:$c\\_\mathsf{Pre}_{i}(N):=\mathsf{True}$;  $\ignorespaces\triangleright$
Cumulative conjoined pre-condition

12:do

13: if {$c\\_\mathsf{Pre}_{i}(N-1)\wedge\psi(N-1)\wedge\partial\varphi(N)$}
$\partial\mathsf{P}_{N}$ {$c\\_\mathsf{Pre}_{i}(N)\wedge\psi(N)$} then

14: return $\mathsf{True}$;  $\ignorespaces\triangleright$ Assertion verified

15: end if

16: $i:=i+1$;

17:
$\mathsf{Pre}_{i}(N-1):=\textsc{LoopFreeWP}(\mathsf{Pre}_{i-1}(N),\partial\mathsf{P}_{N})$;
$\ignorespaces\triangleright$ Dijkstra’s $\mathsf{WP}$ sans $\mathsf{WP}$-for-
loops

18: if no new $\mathsf{Pre}_{i}(N-1)$ obtained then
$\ignorespaces\triangleright$ Can happen if ${\partial\mathsf{P}_{N}}$ has a
loop

19: if CheckProgress($\mathsf{P}_{N}$, $\partial\mathsf{P}_{N}$) then

20: return FPIVerify(${\partial\mathsf{P}_{N}}$,
$c\\_\mathsf{Pre}_{i-1}(N-1)\wedge\psi(N-1)\wedge\partial\varphi(N)$,
$c\\_\mathsf{Pre}_{i-1}(N)\wedge\psi(N)$);

21: else

22: return $\mathsf{False}$;  $\ignorespaces\triangleright$ Failed to prove by
full-program induction

23: end if

24: else

25:
$c\\_\mathsf{Pre}_{i}(N):=c\\_\mathsf{Pre}_{i-1}(N)\wedge\mathsf{Pre}_{i}(N)$;

26: end if

27:while Base case check {$\varphi(1)$} $\mathsf{P}_{1}$
{$c\\_\mathsf{Pre}_{i}(1)$} passes;

28:return $\mathsf{False}$;  $\ignorespaces\triangleright$ Failed to prove by
full-program induction

The basic version of full-program induction algorithm is presented as routine
FPIVerify in Algorithm 7. The important steps of Algorithm 7 include checking
conditions 3(a), 3(b) and 3(c) of Theorem 1 (lines 1, 27 and 13 resp.),
calculating the weakest pre-condition of the relevant part of the post-
condition (line 17), recursively invoking our routine FPIVerify with the
strengthened pre- and post-conditions (line 20), and accumulating the the
weakest pre-condition predicates thus calculated for strengthening the pre-
and post-conditions (line 25). We now discuss the algorithm in detail.

We first check the base case of the analysis in line 1. The base case of our
induction reduces to checking the validity of a Hoare triple of a loop-free
program. This is achieved by compiling the pre-condition, program and post-
condition into a first-order logic formula. The validity of the formula can be
checked with an off-the-shelf back-end SMT solver like Z3. If the check fails,
we have found a valid counter-example that is reported to the user in line 2,
and the algorithm terminates in line 3.

Next, we rename the variables and arrays in the program $\mathsf{P}_{N}$ as
well as the pre- and post-conditions (as described in Sect. 4.1) and collect
the set of glue nodes (line 5). Then, in line 6, we compute the difference
pre-condition $\partial\varphi(N)$ using function SyntacticDiff (described in
Sect. 4.7). We then compute the difference program $\partial\mathsf{P}_{N}$,
in line 7, using function ProgramDiff from Sect. 4.5. Note that this function
can compute the difference program when the scalar variables/arrays of
interest are identified as affected. In line 8, we simplify the statements in
the computed difference program, remove redundant statements and try to
accelerate loops, if any, using function SimplifyDiff from Algorithm 5.

The do-while loop in lines 12–27 iteratively checks if the given assertion can
be proved. Once the base case succeeds, we check the inductive step in line
13. If the loop terminates via the return statement in line 14, then the
inductive claim has been successfully proved. Otherwise, in line 17, we
compute Dijkstra’s weakest pre-condition using the formula
$\mathsf{Pre}_{i}(N)$, over the difference program. The formula
$\mathsf{Pre}_{i}(N)$ is initialized to $\psi(N)$ in line 10. We denote the
computed weakest pre-condition as $\mathsf{Pre}_{i}(N-1)$. Note that, the
formula $\mathsf{Pre}_{i}(N-1)$ strengthens the pre-condition and the same
formula $\mathsf{Pre}_{i}(N)$, but with $N$ substituted for $N-1$, strengthens
the post-condition. The variable $c\\_\mathsf{Pre}_{i}(N-1)$, initialized to
$\mathsf{True}$ in line 11, accumulates weakest pre-condition formulas from
each loop iteration (line 25).

In case no further weakest pre-conditions can be generated, checked in line
18, we recursively invoke FPIVerify on ${\partial\mathsf{P}_{N}}$ in line 20.
Prior to the recursive invocation, we check if it will be beneficial using
function CheckProgress, in line 19. Discussion about CheckProgress is deferred
to Sect. 6. The recursive invocation helps in situations where the computed
difference program ${\partial\mathsf{P}_{N}}$ has loops. To present an example
of this scenario, we modify the program in Fig. 1 by having the statement
C[t3] = N; (instead of C[t3] = 0;) in line $10$. In this case,
${\partial\mathsf{P}_{N}}$ retains a loop that rectifies the value of C[t3]
corresponding to its computation in the third loop in Fig. 1. The recursive
invocation of full-program induction on ${\partial\mathsf{P}_{N}}$ as input
for the example described here will result in a loop-free difference program.
If the check in line 19 reports that further application of full-program
induction will not yield any benefits then we report the failure of our
technique in line 22.

When weakest pre-condition computation succeeds, we conjoin the computed
strengthening predicate $\mathsf{Pre}_{i}(N)$ with the variable
$c\\_\mathsf{Pre}_{i-1}(N)$ in line 25. Since the weakest pre-condition
($\mathsf{Pre}_{i}(N-1)$ in line 17) computed in every iteration of the loop
is conjoined to strengthen the inductive pre-condition
($c\\_\mathsf{Pre}_{i}(N-1)$ in line 25), it suffices to compute the weakest
pre-condition of $\mathsf{Pre}_{i-1}(N)$ (instead of
$c\\_\mathsf{Pre}_{i}(N)\wedge\psi(N)$) in line 17. Possibly multiple
iterations of the loop in lines 12–27 are required to strengthen the pre- and
post-conditions. After each iteration, the base case is checked again in line
27 with the strengthened pre- and post-conditions. If the loop terminates due
to violation of the base-case with the strengthened post-condition (line 27),
we report the failure of our method by returning $\mathsf{False}$ in line 28.

######  Lemma 24.

Upon successful termination, if function FPIVerify returns $\mathsf{True}$,
then $\\{\varphi_{N}\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi_{N}\\}$ holds for all
$N\geq 1$.

Proof: Verifying the given Hoare triple requires establishing the conditions
mentioned in Theorem 1. The functions ProgramDiff invoked in line 7 and
SimplifyDiff invoked in line 8 ensure condition $1$ of Theorem 1 (refer
Theorem 2 and Lemma 22). The call to SyntacticDiff in line 6 in FPIVerify
computes the difference pre-conditions that satisfy conditions $2$(a) and
$2$(b) (refer Lemma 23). The conditions $3$(a) and $3$(b) of Theorem 1 are
checked in lines 1 and 27 respectively. The check in line 13 ensures that the
return statement in line 14 executes only when condition $3$(c) of Theorem 1
is ensured. Similarly, the statement in line 20 returns $\mathsf{True}$ only
if the recursive call to FPIVerify proves all conditions in Theorem 1. Hence,
we conclude that $\\{\varphi_{N}\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi_{N}\\}$
holds for all $N\geq 1$.

###  5.3 Generalized FPI Algorithm

Algorithm 8 FPIDecomposeVerify( i : integer )

1:do

2:
$\langle\mathsf{Pre}_{i}^{\prime}(N-1),\partial\varphi_{i}^{\prime}(N)\rangle$
:= $\textsc{NextDecomposition}(\mathsf{Pre}_{i}(N-1))$;

3: Check if (a)
$\partial\varphi_{i}^{\prime}(N)\wedge\mathsf{Pre}_{i}^{\prime}(N-1)\rightarrow\mathsf{Pre}_{i}(N-1)$,

4: (b)
$\varphi(N)\rightarrow\varphi(N-1)\odot\left(\partial\varphi^{\prime}_{i}(N)\wedge\partial\varphi(N)\right)$,
$\ignorespaces\triangleright$ where $\odot\in\\{\wedge,\vee\\}$

5: (c) $\mathsf{P}_{N-1}$ does not update any variable or array element in
$\partial\varphi_{i}^{\prime}(N)$

6: if any check in lines 3 \- 5 fails then

7: if $\textsc{HasNextDecomposition}(\mathsf{Pre}_{i}(N-1))$ then

8: continue;

9: else

10: return $\mathsf{False}$;

11: end if

12: end if

13: if
{$c\\_\mathsf{Pre}_{i-1}(N-1)\wedge\psi(N-1)\wedge\mathsf{Pre}_{i}(N-1)\wedge\partial\varphi(N)$}
$\partial\mathsf{P}_{N}$
{$c\\_\mathsf{Pre}_{i-1}(N)\wedge\psi(N)\wedge\mathsf{Pre}_{i}^{\prime}(N)$}
then

14: return $\mathsf{True}$;  $\ignorespaces\triangleright$ Assertion verified

15: else

16:
$c\\_\mathsf{Pre}_{i}(N):=c\\_\mathsf{Pre}_{i-1}(N)\wedge\mathsf{Pre}_{i}^{\prime}(N)$;

17:
$\mathsf{Pre}_{i+1}(N-1):=\textsc{LoopFreeWP}(\mathsf{Pre}_{i}^{\prime}(N),\partial\mathsf{P}_{N})$;
$\ignorespaces\triangleright$ Dijkstra’s $\mathsf{WP}$ sans $\mathsf{WP}$-for-
loops

18: if {$\varphi(1)$} $\mathsf{P}_{1}$
{$c\\_\mathsf{Pre}_{i}(1)\wedge\mathsf{Pre}_{i+1}(1)$} holds then

19: $prev\\_\partial\varphi(N)$ := $\partial\varphi(N)$;

20: $\partial\varphi(N)$ :=
$\partial\varphi^{\prime}_{i}(N)\wedge\partial\varphi(N)$;

21: if FPIDecomposeVerify$(i+1)$ then $\ignorespaces\triangleright$ Recursive
invocation

22: return $\mathsf{True}$;  $\ignorespaces\triangleright$ Assertion verified

23: else

24: $\partial\varphi(N)$ := $prev\\_\partial\varphi(N)$;

25: end if

26: end if

27: $i:=i+1$;

28: end if

29:while $\textsc{HasNextDecomposition}(\mathsf{Pre}_{i}(N-1))$;

30:return $\mathsf{False}$;  $\ignorespaces\triangleright$ Failed to prove by
full-program induction

While the algorithm FPIVerify suffices for all of our experiments, it may not
always be the case. Specifically, even if ${\partial\mathsf{P}_{N}}$ is loop-
free, the analysis may exit the loop in lines 12–27 of FPIVerify by violating
the base case check in line 27. To handle (at least partly) such cases, we
propose the following strategy. Whenever a (weakest) pre-condition
$\mathsf{Pre}_{i}(N-1)$ is generated, instead of using it directly to
strengthen the current pre- and post-conditions, we “decompose” it into two
formulas $\mathsf{Pre}_{i}^{\prime}(N-1)$ and
${\partial\varphi_{i}^{\prime}(N)}$ with a two-fold intent: (a) potentially
weaken $\mathsf{Pre}_{i}(N-1)$ to $\mathsf{Pre}_{i}^{\prime}(N-1)$, and (b)
potentially strengthen the difference formula ${\partial\varphi(N)}$ to
${\partial\varphi_{i}^{\prime}(N)}\wedge{\partial\varphi(N)}$. The checks for
these intended usages of $\mathsf{Pre}_{i}^{\prime}(N-1)$ and
${\partial\varphi_{i}^{\prime}(N)}$ are implemented in lines 3, 4, 5, 13 and
18 of routine FPIDecomposeVerify, shown as Algorithm 8. This routine is meant
to be invoked as FPIDecomposeVerify$(i)$ after each iteration of the loop in
lines 12–27 of routine FPIVerify (so that $\mathsf{Pre}_{i}(N)$,
$c\\_\mathsf{Pre}_{i}(N)$ etc. are initialized properly). In general, several
“decompositions” of $\mathsf{Pre}_{i}(N)$ may be possible, and some of them
may work better than others. FPIDecompseVerify permits multiple decompositions
to be tried through the use of the functions NextDecomposition and
HasNextDecomposition. The meaning of both these functions is intuitive from
their names. Lines 21–24 of FPIDecomposeVerify implement a simple back-
tracking strategy, allowing a search of the space of decompositions of
$\mathsf{Pre}_{i}(N-1)$. Observe that when we use FPIDecomposeVerify, we
simultaneously compute a difference formula
$({\partial\varphi^{\prime}_{i}(N)}\wedge{\partial\varphi(N)})$ and an
inductive pre-condition
$(c\\_\mathsf{Pre}_{i-1}(N)\wedge\mathsf{Pre}_{i}^{\prime}(N))$.

######  Lemma 25.

Upon successful termination, if function FPIDecomposeVerify returns
$\mathsf{True}$, then $\\{\varphi_{N}\\}$ $\;\mathsf{P}_{N}\;$
$\\{\psi_{N}\\}$ holds for all $N\geq 1$.

Proof: The conditions mentioned in Theorem 1 are a pre-requisite to verifying
the given Hoare triple. Condition $1$ of Theorem 1 is ensured by difference
computation (functions ProgramDiff and SimplifyDiff) in FPIVerify. Conditions
$2$(a) and $2$(b) are established in FPIVerify (via the call to function
SyntacticDiff) and the checks on lines 3–5 in FPIDecomposeVerify ensure that
these conditions continue to hold. Further, FPIVerify also ensures conditions
$3$(a) and $3$(b) before it invokes FPIDecomposeVerify. Now, the check in line
13 in FPIDecomposeVerify ensures condition $3$(c) of Theorem 1. Similarly, the
statement in line 22 in FPIDecomposeVerify returns $\mathsf{True}$ only if the
recursive call to FPIDecomposeVerify proves all the conditions in Theorem 1.
Hence, we conclude that $\\{\varphi_{N}\\}$ $\;\mathsf{P}_{N}\;$
$\\{\psi_{N}\\}$ holds for all $N\geq 1$.

##  6 Progress Measures

Recall from Sect. 5.2 that given the parameterized Hoare triple
$\\{\varphi(N)\\}$ $\mathsf{P}_{N}$ $\\{\psi(N)\\}$, our technique recursively
computes difference programs until the given post-condition $\psi(N)$ is
proved. The difference computation must eventually result in programs
$\partial\mathsf{P}_{N}$ that can be easily verified without the need of
further applying inductive reasoning or indicate otherwise. In this section,
we define a progress measure that can be used to check if the difference
computation will eventually simplify the program to the extent that it can be
verified using a back-end SMT solver. The measure is based on the
characteristics of the difference programs computed by our technique.

Ranking functions have been traditionally used to show program termination
rank-fun1 ; rank-fun2 ; termination ; lexico-cite . We use the notion of
ranking functions to measure the progress that our technique has made towards
verifying the given post-condition using the difference programs. Several
different criteria have been used in the literature to define ranking
functions. Our ranking function links with each difference program a value
from a well-founded domain. We assign the minimal rank to programs that can be
effectively verified, for example using a back-end SMT solver. A difference
program gets a smaller rank compared to another difference program if it is
“closer” (in a natural way) to programs that can be proved. Here, we list some
criteria that can be used for defining the ranking function for our technique
based on the syntactic changes in difference programs vis-a-vis the given
program.

The main hurdle in proving the given Hoare Triple, $\\{\phi(N)\\}$
$\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$, are the loops in the given program
$\mathsf{P}_{N}$. Once the difference program is loop-free, the post-condition
in such programs can be easily verified by an SMT solver and our technique is
no longer required to recursively apply induction any further for proving such
programs. Thus, the difference programs for which our technique terminates are
loop-free programs and programs in which loops can be accelerated or optimized
away with known techniques. Hence, reduction in the number of loops in the
difference program $\partial\mathsf{P}_{N}$ vis-a-vis the given program
$\mathsf{P}_{N}$ is the main criterion to measure progress in our technique.

Further, the difference computation can potentially reduce the dependence on
the value of $N$. For programs with expressions that do not directly or
indirectly 111By indirect dependence, we mean the dependence via another value
computed in a peeled or non-peeled statements in the program. rely on $N$, the
difference program consists of only the peeled iterations of loops. Clearly,
when the difference program $\partial\mathsf{P}_{N}$ is impervious to the
value of $N$, additional code to rectify the values of variables is no longer
required in the subsequent recursive invocations. This indicates that we have
made progress. We thus use the presence of variables in the program whose
value directly or indirectly depends on the value of $N$ as another criteria
to measure progress. As previously stated in Sect. 4.4, if the value of a
variable/array depends on $N$ or on a value computed in a peeled statement,
then we call such variables/arrays as _affected variables/arrays_. Our
technique computes the set of affected variables during each recursive attempt
to verify the post-condition. The difference program must rectify the values
of these affected variables/arrays. When the difference program has no
affected variables, the verification attempt can be terminated after the next
invocation of our technique.

We also consider the complexity of expressions in the program and use it as a
criteria for measuring progress. For every expression appearing in assignment
statements, its expression complexity can be defined in many possible ways.
Once this complexity is defined for expressions, we can take the maximum
complexity of all the expressions as the expression complexity of the entire
program. For programs with polynomial expressions, we can use the highest
degree of the affected variables/arrays in the expression as the expression
complexity. Similarly, several other criteria can be used to define the
expression complexity. These include nesting levels of array indices,
size/weight of the expression trees in $\partial\mathsf{P}_{N}$ vis-a-vis
$\mathsf{P}_{N}$, number of variables, operators and constants in the
expressions and so on. It is worth pointing out that such notions have been
previously studied in term rewriting systems simporder ; decomporder .

Note that each criterion discussed so far, including the number of loops, the
number of affected variables and the expression complexity, is well-founded.
Hence, the domain of values represented by their Cartesian product is also
well-founded and represents a lexicographic ordering on the difference
programs computed by our method. Progress is guaranteed if each recursive
invocation of our technique in the cycle reduces this measure assigned by such
a ranking function. We argue that the cycle of recursive invocations to our
technique must eventually terminate, as there are no infinite descending
chains of elements in the well-founded domain. We present an algorithm that
can compute values from this domain on the fly and return the result of the
comparison between the computed quantities. Note that no user intervention is
required for checking progress.

Algorithm 9 CheckProgress($\mathsf{P}_{N}$: program, $\partial\mathsf{P}_{N}$:
difference program)

1:$\mathsf{LoopList}$ := Loops($\mathsf{P}_{N}$);

2:$\mathsf{LoopList^{\prime}}$ := Loops($\partial\mathsf{P}_{N}$);

3:if #$\mathsf{LoopList^{\prime}}$ $<$ #$\mathsf{LoopList}$ then

4: return $\mathsf{True}$;

5:end if

6:$\mathsf{AffectedVars}$ := ComputeAffected($\mathsf{P}_{N}$);

7:$\mathsf{AffectedVars}^{\prime}$ :=
ComputeAffected($\partial\mathsf{P}_{N}$);

8:if #$\mathsf{AffectedVars}^{\prime}$ $<$ #$\mathsf{AffectedVars}$ then

9: return $\mathsf{True}$;

10:end if

11:$\mathsf{EC}$ := ExpressionComplexity($\mathsf{P}_{N}$);

12:$\mathsf{EC^{\prime}}$ := ExpressionComplexity($\partial\mathsf{P}_{N}$);

13:if $\mathsf{EC^{\prime}}$ $<$ $\mathsf{EC}$ then

14: return $\mathsf{True}$;

15:end if

16:return $\mathsf{False}$;

The routine CheckProgress in Algorithm 9 is used for checking progress after
the difference program is computed. The algorithm is based on the change in
the number of loops, number of affected variables and the expression
complexity of the given program $\mathsf{P}_{N}$ vis-a-vis the difference
program $\partial\mathsf{P}_{N}$. First, we compute the number of loops in
programs $\mathsf{P}_{N}$ and $\partial\mathsf{P}_{N}$. We compare the number
of loops in $\mathsf{P}_{N}$ and $\partial\mathsf{P}_{N}$ in line 3. If the
difference program has fewer loops than $\mathsf{P}_{N}$, then we return
$\mathsf{True}$ concluding that the $\partial\mathsf{P}_{N}$ is simpler to
verify than the given program. Note that, we do not consider the glue loops in
the difference program that were introduced during the renaming step to copy
values across versions. If the number of loops does not decrease in an
invocation of our technique, we check if the number of affected variables has
decreased. We compute the set of affected variables in $\mathsf{P}_{N}$ and
$\partial\mathsf{P}_{N}$ using the routine ComputeAffected from Algorithm 3.
In line 8, we compare the number of affected variables in both the programs.
The algorithm returns $\mathsf{True}$ if the difference program has fewer
affected variables than $\mathsf{P}_{N}$. Subsequently, we check if the
expressions in the difference program $\partial\mathsf{P}_{N}$ are “simpler”,
and easier to reason with, than $\mathsf{P}_{N}$. We assume the availability
of a routine ExpressionComplexity that can compute this complexity measure for
programs $\mathsf{P}_{N}$ and $\partial\mathsf{P}_{N}$. In line 13 we check if
the expression complexity of the difference program $\partial\mathsf{P}_{N}$
is less than that of the given program $\mathsf{P}_{N}$, in which case the
algorithm returns $\mathsf{True}$. If none of these criteria are met, then the
algorithm returns $\mathsf{False}$.

######  Lemma 26.

If CheckProgress in Algorithm 9 returns $\mathsf{True}$, then the difference
program $\partial\mathsf{P}_{N}$ is “simpler” to verify (using the full-
program induction technique) as compared to the given program
$\mathsf{P}_{N}$.

Proof: The difference program $\partial\mathsf{P}_{N}$ has strictly less loops
than $\mathsf{P}_{N}$ when the check in line 3 is satisfied. In this case,
verifying $\partial\mathsf{P}_{N}$ is simpler than verifying $\mathsf{P}_{N}$.
Further, reduction in the number of affected variables/arrays means less code
is retained to rectify their values. Hence, when the check on line 8 is
satisfied, $\partial\mathsf{P}_{N}$ is simpler than $\mathsf{P}_{N}$. By Lemma
17, when none of the variables/arrays of interest are identified as affected,
only the peeled iterations of loops (referred as
$\mathsf{Peel}({\mathsf{P}_{N}})$) suffice as the difference program
$\partial\mathsf{P}_{N}$. This also makes verifying $\partial\mathsf{P}_{N}$
simpler as compared to $\mathsf{P}_{N}$. Similarly, the last condition ensures
that the expressions in the difference program are easier to reason with than
the given program $\mathsf{P}_{N}$. Further, these characteristics of the
program and the ordering among them as specified by CheckProgress forms a
lexicographic ranking function lexico-cite . Hence, these quantities are bound
to reduce with each application of our technique, making the difference
program simpler to verify each time. This concludes the lemma.

######  Lemma 27.

The routine FPIVerify in Algorithm 7 eventual terminates.

Proof: Function FPIVerify presented in Algorithm 7 can execute in infinite
recursion only when the invocation of CheckProgress in line 19 returns
$\mathsf{True}$ infinitely often. From difference program computation, we know
that the number of loops and affected variables/arrays in the difference
program $\partial\mathsf{P}_{N}$ never increase beyond their counts in the
given program $\mathsf{P}_{N}$, they either decrease or remain the same.
Further, if the expression complexity of all the statements that update an
affected variable/array does not decrease then our method returns
$\mathsf{False}$, and consequently we report failure. Thus, these three
characteristics with the specified ordering among them form a lexicographic
ranking function lexico-cite . Since the value of the lexicographic ranking
function strictly decreases in each recursive application of our method, it
ensures that function FPIVerify eventually terminates.

##  7 Full-program Induction in Generalized Settings

For brevity and ease of explanation, we have presented our technique in simple
settings. We have so far considered Hoare triples that have a single parameter
$N$. In this section, we show how our technique can be adapted to Hoare
triples with multiple parameters as well as peeling loops in different
directions for our inductive reasoning. We also state the limitations of our
technique.

Based on the ideas previously described, our technique can already verify
several interesting scenarios in programs. Our technique can verify programs
that manipulate arrays of different sizes as well as loops with non-uniform
termination conditions that are a linear function of $N$. It does so by
computing a (possibly different) peel count for each loop that manipulates
different arrays. For the ease of presentation, our algorithm computes the
rectified values of variables/arrays in statements with a single operator.
When the program statements have two or more operators, such statements can be
split into multiple statements, by introducing temporary variables such that
each statement has a single operator, and then computing the difference
program using our algorithm.

##### Multiple independent program parameters.

Consider proving Hoare triples with multiple parameters
$N_{1},N_{2},...,N_{k}$. Suppose that the values of these parameters are
independent of each other. Verifying Hoare triples for all values of these
parameters can be done by inducting on one program parameter at a time while
keeping the other parameters fixed. We explain this with the help of a simple
example with two parameters. To prove that the Hoare Triple
$\\{\varphi(N_{1},N_{2})\\}$ $\;\mathsf{P}_{N_{1},N_{2}}\;$
$\\{\psi(N_{1},N_{2})\\}$ for all $N_{1}\geq a\wedge N_{2}\geq b$, we prove
the following three sub-goals. First, in the base-case we prove that the
triple $\\{\varphi(a,b)\\}$ $\;\mathsf{P}_{a,b}\;$ $\\{\psi(a,b)\\}$ holds.
Second, induction over the parameter $N_{1}$, where we assume the Hoare Triple
$\\{\varphi(k,N_{2})\\}$ $\;\mathsf{P}_{k,N_{2}}\;$ $\\{\psi(k,N_{2})\\}$
holds with $k\geq a\wedge N_{2}\geq b$, and prove the Hoare Triple
$\\{\varphi(k+1,N_{2})\\}$ $\;\mathsf{P}_{k+1,N_{2}}\;$
$\\{\psi(k+1,N_{2})\\}$, treating $N_{2}$ as a symbolic parameter unchanged
during the induction. Third, induction over the parameter $N_{2}$, where we
assume that the Hoare Triple $\\{\varphi(N_{1},l)\\}$
$\;\mathsf{P}_{N_{1},l}\;$ $\\{\psi(N_{1},l)\\}$ holds where $N_{1}\geq
a\wedge l\geq b$, and prove the Hoare Triple $\\{\varphi(N_{1},l+1)\\}$
$\;\mathsf{P}_{N_{1},l+1}\;$ $\\{\psi(N_{1},l+1)\\}$, treating $N_{1}$ as a
symbolic parameter unchanged in the induction. This can be easily extended to
Hoare triples with more than two parameters. For programs that manipulate
arrays of different independent sizes, we treat each variable representing the
symbolic size of arrays as a parameter. As described above, our technique
verifies such programs by inducting on each parameter one at a time.

##### Different direction of peeling loops.

Recall that the difference program $\partial\mathsf{P}_{N}$ is sequentially
composed with $\mathsf{P}_{N-1}$. Earlier, we have been peeling the last
iterations of the loops in $\mathsf{P}_{N}$ so that $\mathsf{P}_{N-1}$ and
$\mathsf{P}_{N}$ have the same number of iterations in each loop. However,
there are programs where peeling the last iterations of loops may not be
possible such that our technique can compute a difference program. In such
cases, we may need to peel the initial iterations of the loops in the program.
As an example, consider a loop where the value of the loop counter decreases
in each iteration. A possible way is to rotate these loops to fit the template
of loops defined in our grammar and then apply our technique. However, not all
loops are such that they can be rotated easily using the standard loop
transformation techniques. For such loops, we may need to peel it at the
beginning. We peel the initial iterations of these loops and add the code that
rectifies values of variables computed in the loop after the peeled iterations
such that $\mathsf{P}_{N-1}\mathchar 24635\relax\;\partial\mathsf{P}_{N}$ is
semantically equivalent to $\mathsf{P}_{N}$. Thus, by peeling initial
iterations of loops when computing the difference program, our technique can
be easily adapted to programs with such loops in a sound way.

###  7.1 Limitations

There are several scenarios under which the full-program induction technique
may not produce a conclusive result.

Program computation with side-effects may make it difficult to compute the
difference program such that there is a clear separation between the program
$\mathsf{P}_{N-1}$ and the rest of the computation that can make up $P_{N}$.
Computation that results in side-effects includes I/O operations, allocation,
de-allocation and modification of heap memory and other operations that modify
the environment which is not local to the given program. When the given
program is not free of such side-effects, our technique may not be able to
decompose it into $\mathsf{P}_{N-1}$ and $\partial\mathsf{P}_{N}$. Note that
we only disallow the computation that impacts the post-condition to be proved.
In our experience, a large class of array manipulating programs are naturally
free of side-effects. In particular, the programs discussed in this paper
(including Fig. 1) and those used for experimentation are free of side-
effects.

Currently our technique is unable to verify programs with branch conditions
that are dependent on the parameter $N$. Computing the difference program
becomes cumbersome in such cases. This stems from the fact that the branch
condition may evaluate to different outcomes in $\mathsf{P}_{N}$ and
$\mathsf{P}_{N-1}$, for the same value of $N$, and hence, may require us to
compute the difference of two arbitrary pieces of code blocks. We identify
such cases while computing the difference program in Algorithm 4 and suspend
our verification attempt on line 7 of the routine NodeDiff. Note that this
does not include the loop conditions, which are handled by peeling the loop.
To illustrate this case, consider the Hoare triple shown in Fig. 26. The first
loop in the program initializes array A and the second loop updates array A
within a branch statement with the conditional expression N%2 == 0. It is easy
to see that this branch condition will evaluate to different outcomes in
$\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$. As a result, it is difficult for our
technique to compute a difference program. Invariant generation techniques may
be better suited for verifying this example. The weakest loop invariants
needed to prove the post-condition in this example are: $\forall
j\in[0,i)\;(A[j]=0)$ for the first loop and $\forall
k\in[0,i)\;(A[k]\%2=N\%2)$ for the second loop.

    // assume(

    $\ignorespaces\mathsf{True}$

    )

    1.  for(i=0; i<N; i++) {
    2.    A[i] = 0;
    3.  }

    5.  for(i=0; i<N; i++) {
    6.    if( N%2 == 0 ) {
    7.      A[i] = A[i] + 2;
    8.    } else {
    9.      A[i] = A[i] + 1;
    10.   }
    11. }

    // assert(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

     [0,N), A[i]%2 = N%2)

Figure 26: Challenge example

The difference program includes all peeled iterations of $\mathsf{P}_{N}$ that
are missed in $\mathsf{P}_{N-1}$. Hence, our technique needs to know the
symbolic upper bound on the value of the loop counter to be able to compute
the number of iterations to be peeled from the program. Further, when programs
have loops with non-linear termination conditions, the construction of the
difference program becomes challenging. The number of peeled iterations itself
may be a function of $N$ and possibly result in a loop in the difference
program. For example, consider a loop in $\mathsf{P}_{N}$ with the counter $i$
initialized to $0$ and the loop termination condition “$i<N^{2}$”. The
corresponding loop in $\mathsf{P}_{N-1}$ has the same initialization but the
termination condition is “$i<(N-1)^{2}$”. “$2\times N+1$” iterations must be
peeled from this loop. For such loop conditions, an entire loop appears as the
peel in the difference program. Since the number of iterations to be peeled is
not a constant number, currently while computing this peel (in line 7 of
Algorithm 1), our technique reports a failure to handle such programs.
Further, our grammar restricts the shape of loops that can be verified using
our technique. Most notably, we analyze programs with only non-nested loops.
We have designed a variant of the full-program induction technique diffy-cav21
that can verify a class of programs with nested loops. The technique greatly
simplifies the computation of difference programs. It infers and uses
relations between two slightly different versions of the program during the
inductive step. We refer the interested reader to diffy-cav21 .

The inductive reasoning may remain inconclusive when the rank of the
difference programs, as defined in Sect. 6, does not reduce during the
successive invocations to verify the post-condition using our technique.
Continuous reduction in the rank/progress measure is crucial to the success of
full-program induction. When no progress is observed, we suspend the
verification attempt in line 22 of the routine FPIVerify in Algorithm 7.
Though the ranking functions can be defined in many possible ways, there are
programs that pose a challenge in computing the difference program in a way
that the rank of the computed difference program does not reduce. However,
such programs are rarely seen in practice.

Our technique may fail to verify a correct program if the heuristics used for
weakest pre-condition either fail or return a pre-condition that causes
violation of the base-case checked on line 27 of the routine FPIVerify in
Algorithm 7.

Apart from the conceptual limitations mentioned above, our prototype
implementation has a few limitations. We currently support expressions in
assignment statements with only $\\{+,-,\times,\div\\}$ operators. In the
implementation we support a single program parameter and peel only the last
iterations of loops. Despite all these limitations, our experiments show that
full-program induction performs remarkably well on a large suite of
benchmarks.

##  8 Experimental Results

In this section, we present an extensive experimental evaluation of the _full-
program induction_ technique on a large set of array manipulating benchmarks.

###  8.1 Implementation

We have implemented our technique in a prototype tool called Vajra. Our tool
and the benchmarks used in the experiments are publicly available at vajra-
artifact . Vajra takes a C program in SV-COMP format as input. The tool,
written in C++, is built on top of the LLVM/CLANG clang  $6.0.0$ compiler
infrastructure. We use CLANG front-end to obtain LLVM bitcode. Several
normalization passes such as constant propagation, dead code elimination,
static single assignment (SSA) generation for renaming variables and arrays,
loop normalization for running loop-dependent passes that identify program
constructs such as loop counter, lower bound and upper bound expressions,
branch conditions and so on, are performed on the bitcode. We use Z3 z3
v$4.8.7$ as the SMT solver to prove the validity of the parametric Hoare
triples for loop-free programs and to compute weakest pre-conditions. We have
also implemented a Gaussian elimination based procedure that propagates array
equalities and simplifies select store nests in the generated SMT formula to
compute weakest pre-conditions.

###  8.2 Benchmarks

We have evaluated Vajra on a test-suite of $231$ benchmarks inspired from
different algebraic functions that compute polynomials as well as a standard
array operations such as copy, min, max and compare. Of these there are $121$
safe benchmarks and $110$ unsafe benchmarks. All our programs take a symbolic
parameter $N$ which specifies the size of each array as well as the number of
times each loop executes. Several benchmarks in the test-suite follow
different types of templates wherein either the number of loops in the program
increases or they use potentially different data values. Program from the
first kind of templates allow us to gauge the scalability aspect of our
technique as the number of loops in the program increases. Programs from the
latter templates allow for checking the robustness of our technique to the
content of arrays and scalars.

Assertions in the benchmarks are either universally quantified or quantifier
free safety properties. The predicates in these assertions are (in-)equalities
over scalar variables, array elements, and possibly non-linear polynomial
terms over $N$. Although our technique can handle some classes of
existentially quantified assertions as discussed in Sect. 4.7, all the
examples considered for our experiments have universally quantified or
quantifier-free assertions. The approach described in the paper is naturally
applicable to programs with such assertions, given that the underlying SMT
solver can discharge the verification conditions containing formulas with
existential quantification and quantifier alternation when a loop-free
difference program is automatically computed. Handling post-conditions with
existential quantification and quantifier alternation are part of future work.

###  8.3 Setup

All experiments were performed on a Ubuntu 18.04 machine with 16GB RAM and
running at 2.5 GHz. We have compared our tool Vajra against the verifiers for
array programs VIAP (v1.1) viap , VeriAbs (v1.3.10) veriabs20 , Booster (v0.2)
booster , Vaphor (v1.2) vaphor  and FreqHorn (v.0.5) freqhorn . C programs
were manually converted to mini-Java as required by Vaphor and CHC formulae as
required by FreqHorn. Since FreqHorn does not automatically find
counterexamples, so we used the supplementary tool expl from its repository on
unsafe benchmarks as recommend by them. We have used the same version of
VeriAbs that was used to perform the experiments in tacas20 , since the later
version of VeriAbs invokes our tool Vajra in its pipeline for verifying array
programs (refer veriabs20 ). A timeout of $100$ seconds was set for these
experiments.

Tool | Success | CE | Inconclusive | TO
---|---|---|---|---
|  | Safe |  |
Vajra | 110 | 0 | 11 | 0
VIAP | 58 | 0 | 2 | 61
VeriAbs | 50 | 1 | 0 | 70
Booster | 36 | 27 | 17 | 41
VapHor | 27 | 9 | 2 | 83
FreqHorn | 26 | 0 | 19 | 76
|  | Unsafe |  |
Vajra | 0 | 109 | 1 | 0
VIAP | 1 | 108 | 0 | 1
VeriAbs | 0 | 102 | 0 | 8
Booster | 0 | 84 | 15 | 11
VapHor | 1 | 106 | 1 | 2
FreqHorn | 0 | 99 | 0 | 11
Figure 27: Summary of the experimental results

###  8.4 Summary of the Results

We executed all six tools on the entire set of $231$ benchmarks. A table with
the summary of obtained results is shown in Fig. 27. We present the results on
safe and unsafe benchmarks separately for a fair representation of each tool
on the set of benchmarks.

$0$$20$$40$$60$$80$$100$$120$$0$$20$$40$$60$$80$$100$#BenchmarksTime
(s)VajraVIAPVeriAbsBoosterVaphorFreqHorn Figure 28: Quantile plot showing the
performance of all the tools on safe benchmarks
$0$$20$$40$$60$$80$$100$$0$$20$$40$$60$$80$$100$#BenchmarksTime
(s)VajraVIAPVeriAbsBoosterVaphorFreqHorn Figure 29: Quantile plot showing the
performance of all the tools on unsafe benchmarks

###  8.5 Analysis on Safe Benchmarks

Vajra verified $110$ safe benchmarks, compared to $58$ verified by VIAP, $50$
by VeriAbs, $36$ by Booster, $27$ by Vaphor and $26$ by FreqHorn. Vajra was
inconclusive on $11$ benchmarks. The reasons for the inability of our tool to
generate a conclusive result are as follows: (1) the difficulty in computing a
difference program due to the presence of a branch condition dependent on $N$
or complex operations such as modulo, (2) difficulty in computing the required
strengthening of the pre- and post-conditions and (3) the back-end SMT solver
returning an inconclusive result.

Vajra verified $52$ benchmarks on which VIAP diverged, primarily due to the
inability of VIAP’s heuristics to get closed form expressions. VIAP verified
$5$ benchmarks that could not be verified by the current version of Vajra due
to syntactic limitations. Vajra, however, is two orders of magnitude faster
than VIAP on programs that were verified by both (refer Fig. 28).

Vajra proved $60$ benchmarks on which VeriAbs diverged. VeriAbs ran out of
time on programs where loop shrinking and merging abstractions were not strong
enough to prove the assertions. VeriAbs reported $1$ program as unsafe due to
the imprecision of its abstractions and it proved $3$ benchmarks that Vajra
could not.

Vajra verified $74$ benchmarks that Booster could not. Booster reported $27$
benchmarks as unsafe due to imprecise abstractions, its fixed-point
computation engine reported unknown result on $17$ benchmarks and it ended
abruptly on $41$ benchmarks. Booster also proved $2$ benchmarks that could not
be handled by the current version of Vajra due to syntactic limitations.

Vajra verified $83$ benchmarks that Vaphor could not. The distinguished cell
abstraction technique implemented in Vaphor is unable to prove safety of
programs, when the value at each array index needs to be tracked. Vaphor
reported $9$ programs unsafe due to imprecise abstraction, returned unknown on
$2$ programs and ended abruptly on $83$ programs. Vaphor proved $2$ benchmarks
that Vajra could not.

Vajra verified $84$ programs on which FreqHorn diverged, especially when
constants and terms that appear in the inductive invariant are not
syntactically present in the program. FreqHorn ran out of time on $76$
programs, reported unknown result or ended abruptly on $19$ benchmarks.
FreqHorn verified a benchmark with a single loop that Vajra could not.

All the benchmarks that are uniquely solved by Vajra have multiple
sequentially composed loops and/or a form of aggregation/cross-iteration
dependence via a scalar variable or an array.

###  8.6 Analysis on Unsafe Benchmarks

Vajra disproved $109$ benchmarks, compared to $108$ disproved by VIAP, $102$
by VeriAbs, $84$ by Booster, $106$ by Vaphor and $99$ by expl, the
supplementary tool that comes with FreqHorn. Vajra was unable to disprove $1$
benchmark.

Vajra disproved $1$ benchmark which VIAP could not. VIAP concluded $1$
benchmark as safe and timed out on $1$ benchmark. Even on unsafe benchmarks,
Vajra, is an order of magnitude faster than VIAP (refer Fig. 29). Vajra
disproved $7$ benchmarks which VeriAbs could not. VeriAbs ran out of time on
$8$ programs.

Vajra disproved $25$ benchmarks that Booster could not. Booster reported
unknown result on $15$ benchmarks and it timed out on $11$ benchmarks. Vajra
disproved $3$ benchmarks that Vaphor could not. Vaphor proved $1$ program as
safe, returned unknown on $2$ programs and timed out on $2$ programs. Vajra
disproved $10$ programs which expl could not. expl ran out of time on $11$
programs.

###  8.7 Comparing the Performance

Instance | Loops | zerosum | zerosum-const | zerosum-m | zerosum-const-m
---|---|---|---|---|---
1 | 3 | 0.54 | 0.49 | – | –
2 | 5 | 0.87 | 0.88 | 0.86 | 0.92
3 | 7 | 1.28 | 1.27 | 1.26 | 1.21
4 | 9 | 1.73 | 1.94 | 2.07 | 1.76
5 | 11 | 2.32 | 2.56 | 2.31 | 2.48
6 | 13 | – | – | 2.94 | 2.95
Figure 30: Template-wise analysis of the results for the ‘zerosum’ benchmarks

The quantile plots in Figs. 28 and 29 show the performance of each tool on all
the safe and unsafe benchmarks respectively in terms of time taken to produce
the result. Vajra verified/disproved each benchmark within three seconds. In
comparison, as seen from the plots, other tools took significantly more time
in proving the programs.

As mentioned previously, the test-suite has several benchmarks that are
instantiated from different templates. For such instantiated benchmarks that
only change the data values in the instances of the templates, we did not see
any change in the performance of Vajra. Hence, we do not discuss them further.
We now discuss the results for a set of templates where the number of loops in
the benchmarks instantiated from them increases. In Fig. 30, we present the
results of executing Vajra on the benchmarks instantiated from the ‘zerosum’
templates. The first column indicates the benchmark instance number, the
second column indicates the number of loops in the instantiated benchmark,
columns three to six indicate the benchmark template name that is instantiated
and give the time (in seconds) taken by Vajra to prove the given assertion in
the benchmark instance. It can be seen from the table that as the number of
loops increase in the benchmark, our tool requires more time in solving the
benchmark. This is primarily attributed to pre- and post-condition
strengthening step in our technique that requires our technique to infer and
prove auxiliary predicates iteratively during the inductive step.

##  9 Related Work

Earlier work on inductive techniques can be broadly categorized into those
that require loop-specific invariants to be provided or automatically
generated, and those that work without them. Requiring a “good” inductive
invariant for every loop in a program effectively shifts the onus of assertion
checking to that of invariant generation. Among techniques that do not require
explicit inductive invariants or mid-conditions for each loop, there are some
that require loop invariants to be implicitly generated by a constraint
solver. These include techniques based on constrained Horn clause solving chc
; quic3 ; freqhorn ; vaphor , acceleration and lazy interpolation for arrays
booster  and those that use inductively defined predicates and recurrence
solving trace20 ; viap ; aligators , among others.

QUIC3 quic3 , FreqHorn freqhorn  and the technique in chc  infer universally
quantified inductive invariants of array programs specified as Constrained
Horn Clauses. QUIC3 quic3  extends the IC3 framework to a combination of SMT
theories and performs lazy quantifier instantiations. FreqHorn freqhorn
infers universally quantified invariants over arrays within its syntax-guided
synthesis framework and can reason with complex array index expressions by
adopting the _tiling_ sas17  ideas.

Vaphor vaphor  transforms array programs to array-free Horn formulas. Their
technique is parameterized by the number of array cells to be tracked
resulting in an eager quantifier instantiation.

Booster booster  combines acceleration acceleration1 ; acceleration2  and lazy
abstraction with interpolation for arrays lazyabsarray . Performing
interpolation to infer universally quantified array properties is difficult
Jhala ; Monniaux2015 . The technique does not always succeed, especially for
programs where simple interpolants are difficult to compute sas17 .

VIAP viap  translates the program to an array-free quantified first order
logic formula in the theory of equality and uninterpreted functions using the
scheme proposed in viaptheory . They use several tactics to simplify the
generated formula and apply induction over array indices to prove the
property. Unlike our method, it does not have heuristics for finding
additional pre-conditions that are required for the induction proof to succeed
which our method successfully infers.

trace20  uses theorem provers to introduce and prove lemmas that implicitly
capture inductive loop invariants at arbitrary points in the program described
in trace logic.

Thanks to the impressive capabilities of modern constraint solvers and the
effectiveness of carefully tuned heuristics for stringing together multiple
solvers, approaches that rely on constraint solving have shown a lot of
promise in recent years. However, at a fundamental level, these formulations
rely on solving implicitly specified loop invariants garbed as constraint
solving problems.

Template-based techniques Gulwani ; Srivastava09 ; Dirk07  search for
inductive invariants by instantiating the parameters of a fixed set of
templates within the abstract interpretation framework. They can generate
invariants with alternating quantifiers, however, the user must supply
invariant templates and the cost of generating invariants is quite high.

A large number of techniques have been proposed in literature that use
induction ind-bdds ; ind-wsst ; ind-tempo ; ind-tlm ; ind-te ; ind-smt ; ind-
hc  and its pragmatically more useful version k-induction kind ; kind-rtv ;
kind-lustre ; kind-race ; kind-par ; kind-comb ; kind-boost ; kind-kinvs ;
kind-bmc ; kind-interpol ; kind-invinf ; kind-hmc . These techniques generate
and use loop invariants, especially when aimed at verifying safety properties
of programs. In contrast, our novel technique does not rely on generation or
use of loop-specific invariants and differs significantly from these methods
in the way in which the inductive step is formulated using the computed
difference programs and difference pre-conditions.

There are yet other inductive techniques, such as that in lopstr12 ; sas17 ;
squeezing ; diffy-cav21 , that truly do not depend on loop invariants being
generated. In fact, the technique of lopstr12  comes closest to our work in
principle. However, lopstr12  imposes severe restrictions on the input
programs to move the peel of one loop across the next sequentially composed
loop such that the program with the peeled loops composed with the program
fragment consisting of only the peeled iterations is semantically equivalent
to the input program. They call these restrictions on the input programs as
_commutativity of statements_. In practice, such restrictive conditions and
data dependencies are not satisfied by a large class of programs. For
instance, the example in Fig. 1 and our running example in Fig. 4 do not meet
these restrictions. The technique of lopstr12  is thus applicable only to a
small part of the program-assertion space over which our technique works.

The tiling sas17  technique for verifying universally quantified properties of
array programs reasons one loop at a time and applies only when loops have
simple data dependencies across iterations (called _non-interference_ of tiles
in sas17 ). It effectively uses a slice of the post-condition of a loop as an
inductive invariant. In the case of sequentially composed loops, it also
requires strong enough mid-conditions to be automatically generated or
supplied by the user. Our full-program induction technique circumvents all of
these requirements.

The method proposed in squeezing  proves programs correct by induction on a
rank, chosen as the size of program states. It constructs a safety proof by
automatically synthesizing a squeezing function that can map higher-ranked
states to a lower-ranked state, while ensuring that original states are
faithfully simulated by their squeezed counterparts. This allows the method to
shrink program traces of unbounded length, limiting the reasoning to only
minimally-ranked states. A guess-and-check approach combined with heuristics
for making educated guesses is employed for computing the squeezing functions
necessary to prove a given program. Successful synthesis of a squeezing
function is equivalent to establishing the inductive step. These functions can
be quite useful in practice, for example, to prove programs that may not have
a first-order representable loop invariant. In general, squeezing functions
are not easy to synthesize and automatically searching for such functions is a
non-trivial and an exceedingly time consuming task. Further, the squeezing
functions can only consist of commutative and invertible operations,
restricting their applicability. The technique may be used in tandem with the
classical loop invariant based methods. In comparison, our technique generates
and uses difference invariants in an explicit inductive step and it does not
rely on generation and use of squeezers to shrink the state space of the
program.

The technique presented in diffy-cav21  also performs induction on the entire
program and is a parallel line of work. As stated in diffy-cav21 , full-
program induction forms the basis of their technique but the way in which the
inductive step is formulated differs significantly from ours. It coins
difference invariants that relate two slightly different versions of the given
program. They use just the peeled iterations of loops as difference programs
and amend the inductive reasoning using difference invariants. The technique
supports nested loops as well as branch conditions with value dependent on the
program parameter $N$. The prototype tool Diffy diffy  implements the method.
We believe that there are programs for which diffy-cav21  may not be able to
successfully infer and use difference invariants, but full-program induction
(with its recursive invocation ability) will be able to verify the post-
conditions in such programs.

There are several techniques that approximate program computation during
verification. prophecytacas21  has proposed a counterexample-guided
abstraction refinement scheme for programs that manipulate arrays. Their idea
relies on prophecy variables to refine the abstraction. VeriAbs veriabs20  is
an abstraction-based verifier to prove properties of programs. It implements a
portfolio of abstractions that enable the tool to leverage bounded model
checking. These abstractions tend to restrict the array manipulating loops to
a fixed number of (possibly initial) iterations. The tool makes a series of
attempts to prove the property and uses program features to choose the next
abstraction/strategy to be applied. Fluid updates fluid  uses bracketing
constraints, which are over- and under-approximations of indices, to specify
the concrete elements being updated in an array without explicit partitioning.
While their abstraction is independent of the given property, they assume that
only a single index expression updates the array in each loop, severely
restricting the technique. Analyses proposed in Gopan ; Halbwachs  partition
the array into symbolic slices and abstracts each slice with a numeric scalar
variable. Abstract interpretation based techniques Rival ; ArrayCousotCL11
propose an abstract domain which utilizes cell contents to split array cells
into groups. In particular, the technique in Rival  is useful when array cells
with similar properties are non-contiguously present in the array. These
approaches require the implementation of abstract transformers for each
specialized domain which is not a necessity with our framework. Other
techniques for analyzing array manipulating programs include Jhala ; verifast
.

Program differencing paige-differencing , program integration integration  and
differential static analysis dsa-hoare  have been studied in literature for
various purposes. Incremental computation of expensive expressions liu-
incrementalization , optimizing the execution time of programs that manipulate
arrays liu-optimization , reducing the cost of regression testing diff-testing
and checking data-structure invariants ditto07  are some applications of such
techniques. SymDiff symdiff  tool, based on differential static analysis dsa-
hoare , displays semantic differences between different program versions and
checks equivalence. However, the method neither supports checking quantified
post-conditions nor does it support loops and arrays of potentially unbounded
size. Unfortunately, these techniques do not always generate code fragments
that are well suited for property verification, especially when the input
programs manipulate arrays. To the best of our knowledge, full-program
induction is the first technique to successfully employ difference computation
customized for verification in an inductive setting.

Full-program induction also offers several other advantages over the existing
techniques. For instance, it can reason with different quantifiers over
multiple variables, it does not require implementation of specialized abstract
domains for handling quantified formulas and it can enable the use of existing
tools and techniques for reasoning over arrays. We believe that verification
tools need to have an arsenal of techniques to be able to efficiently prove a
wide range of challenging problems. Our novel technique, full-program
induction, is a suitable fit for such an arsenal and has been adopted by
verifiers such as VeriAbs in practice. Since the 2020 edition of the
international software verification competition (SV-COMP), VeriAbs veriabs20
invokes our tool Vajra in its pipeline of tools for verifying programs with
arrays from the set of benchmarks in the competition.

##  10 Conclusion & Future Work

We presented a novel property-driven verification technique, called full-
program induction, that performs induction over the entire program via
parameter $N$. Significantly, our analysis obviates the need for loop-specific
invariants during verification. The technique automatically computes the
difference program and difference pre-condition that enable the inductive step
of the reasoning. Our technique is general and can be applied to programs
manipulating arrays that store integers, matrices, polynomials, vectors and so
on. This give our technique the potential of verifying apis used in machine
learning and cryptography libraries. Experiments show that Vajra performs
remarkably well vis-a-vis state-of-the-art tools for analyzing array
manipulating programs.

Possible directions of future work include investigations into possible ways
of incorporating automatically generated and externally supplied invariants
during our analysis, especially for computing simpler difference programs and
handling programs with nested loops. Automated support for handling assertions
with existential quantification and quantifier alternation and for verifying
heap-manipulating programs as well as programs that operate on tensors using
our technique. Investigations into the use of synthesis-based techniques for
automatically computing the difference programs and adapting them to programs
from various interesting domains forms another line of work. Improvements to
the algorithms for simultaneous strengthening of pre- and post-conditions can
be considered.

## References

  *   * (1) Sheeran, M., Singh, S., Stlmarck, G.: Checking safety properties using induction and a SAT-solver. In: Proc. of FMCAD, pp. 127–144 (2000)
  * (2) Komuravelli, A., Bjorner, N., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using Horn clauses over integers and arrays. In: Proc. of FMCAD, pp. 89–96 (2015)
  * (3) Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proc. of ATVA, pp. 248–266 (2018)
  * (4) Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided-synthesis. In: Proc. of CAV, pp. 259–277 (2019)
  * (5) Rajkhowa, P., Lin, F.: Extending VIAP to handle array programs. In: Proc. of VSTTE, pp. 38–49 (2018)
  * (6) Henzinger, T.A., Hottelier, T., Kovács, L., Rybalchenko, A.: Aligators for arrays (tool paper). In: Proc. of LPAR, pp. 348–356 (2010)
  * (7) Afzal, M., Chakraborty, S., Chauhan, A., Chimdyalwar, B., Darke, P., Gupta, A., Kumar, S., Babu M, C., Unadkat, D., Venkatesh, R.: Veriabs : Verification by abstraction and test generation (competition contribution). In: Proc. of TACAS, pp. 383–387 (2020)
  * (8) Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs by Tiling. In: Proc. of SAS, pp. 428–449 (2017)
  * (9) Monniaux, D., Gonnord, L.: Cell Morphing: From array programs to array-free horn clauses. In: Proc. of SAS, pp. 361–382 (2016)
  * (10) Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: Proc. of ATVA, pp. 18–23 (2014)
  * (11) Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. FMSD 19(1), 7–34 (2001)
  * (12) de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proc. of TACAS, pp. 337–340 (2008)
  * (13) Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Proc. of POPL, pp. 338–350 (2005)
  * (14) Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Proc. of PLDI, pp. 339–348 (2008)
  * (15) Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: Proc. of VMCAI, pp. 282–299 (2015)
  * (16) Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proc. of POPL, pp. 105–118 (2011)
  * (17) Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proc. of POPL, pp. 235–246 (2008)
  * (18) Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. ACM Sigplan Notices 44(6), 223–234 (2009)
  * (19) Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Proc. of VMCAI, pp. 378–394 (2007)
  * (20) Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Proc. of CAV, pp. 193–206 (2007)
  * (21) Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Proc. of FME, pp. 500–517 (2001)
  * (22) Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1-3), 35–45 (2007)
  * (23) Lattner, C., Adve, V.: Llvm: A compilation framework for lifelong program analysis & transformation. In: Proc. of CGO, pp. 75–86 (2004)
  * (24) Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: Proc. of TACAS, pp. 22–39 (2020)
  * (25) Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proc. of POPL, pp. 12–27 (1988)
  * (26) Knobe, K., Sarkar, V.: Array SSA form and its use in parallelization. In: Proc. of POPL, pp. 107–120 (1998)
  * (27) Unadkat, D.P.: Techniques for Precise and Scalable Verification of Array Programs. PhD thesis, Indian Institute of Technology Bombay (2022)
  * (28) Towle, R.A.: Control and Data Dependence for Program Transformations. Ph.D. dissertation, University of Illinois at Urbana-Champaign, USA (1976)
  * (29) Kuck, D.L.: Structure of Computers and Computations. John Wiley & Sons, Inc., USA (1978)
  * (30) Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. TOPLAS 9(3), 319–349 (1987)
  * (31) Horwitz, S., Reps, T.: The use of program dependence graphs in software engineering. In: ICSE, pp. 392–411 (1992)
  * (32) Kennedy, K., Allen, J.R.: Optimizing Compilers for Modern Architectures: A Dependence-based Approach, (2001)
  * (33) Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification, pp. 1–8 (2000)
  * (34) Colón, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Proc. of TACAS, pp. 67–81 (2001)
  * (35) Colón, M.A., Sipma, H.B.: Practical methods for proving program termination. In: Proc. of CAV, pp. 442–454 (2002)
  * (36) Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proc. of VMCAI, pp. 239–251 (2004)
  * (37) Dershowitz, N.: Orderings for term-rewriting systems. Theoretical computer science 17(3), 279–301 (1982)
  * (38) Lescanne, P.: Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems. RAIRO. Informatique théorique 16(4), 331–347 (1982)
  * (39) Chakraborty, S., Gupta, A., Unadkat, D.: Diffy: Inductive reasoning of array programs using difference invariants. In: Proc. of CAV, pp. 911–935 (2021)
  * (40) Chakraborty, S., Gupta, A., Unadkat, D.: Verifying Array Manipulating Programs with Full-program Induction - Artifacts TACAS 2020. figshare https://doi.org/10.6084/m9.figshare.11875428.v1 (2020)
  * (41) Georgiou, P., Gleiss, B., Kovács, L.: Trace logic for inductive loop reasoning. In: Proc. of FMCAD, pp. 255–263 (2020)
  * (42) Bozga, M., Iosif, R., Konecný, F.: Fast acceleration of ultimately periodic relations. In: Proc. of CAV, pp. 227–242 (2010)