11institutetext: LMU Munich, 11email<EMAIL_ADDRESS>
⇒$\Rightarrow$ ⟶$\longrightarrow$ ⟷$\longleftrightarrow$ ⟹$\Longrightarrow$
⟦$\llbracket$ ⟧$\rrbracket$ ∀$\forall$ ∃$\exists$ λ$\lambda$ ⋀$\bigwedge$
∧$\land$ ¬$\lnot$

# A Complete Approach to Loop Verification
with Invariants and Summaries

Gidon Ernst

###### Abstract

Loop invariants characterize the partial result computed by a loop _so far_ up
to an intermediate state. It has been noted, however, that complementing
invariants by _summaries_ , which characterize the _remaining iterations_ of a
loop, can often lead to simpler correctness proofs. In this paper, we derive
sound verification conditions for this approach, and moreover characterize
completeness relative to a class of “safe” invariants, alongside with
fundamental and novel insights in the relation between invariants and
summaries. All theoretical results have immediate practical consequences for
tool use and construction. Summaries should therefore be regarded as a
principal alternative to invariants. To substantiate this claim
experimentally, we evaluate the automation potential using state-of-the-art
Horn solvers, which shows that the the proposed approach is competitive, even
without specialized solving strategies.

##  1 Introduction

Loop invariants [31] are the standard approach to verify programs with loops.
The technique is elegant, theoretically complete wrt. predicate logic with
fixpoints or recursive definitions, and practically successful for both
specifying and verifying loops in automated tools. Recently, inferring such
invariants from a system of Horn-clauses has become popular [8], which affords
a concise presentation of verification tasks and offers concrete algorithmic
leverage for solvers.

The corresponding proof obligations propagate invariants forwards over a
single arbitrary iteration, and soundness is justified by the induction
principle of the least fixpoint of the loop (for partial correctness). Proofs
by induction in general, however, admit an additional backwards reasoning
step, which lifts the conclusion reached after applying the inductive
hypothesis for residual iterations backwards, to cover that particular
iteration, too. The standard proof rule for invariants critically hides access
to that reasoning step (cf. Tuerk [55]). As a practical consequence, sometimes
additional predicates have to be specified solely for the purpose of encoding
the partial execution prefix of a loop as an invariant.

A well-known solution is to specify loops in terms of a contract consisting of
a precondition (effectively an invariant) and a postconditon (called “summary”
here), where the latter may often capture key correctness properties of a loop
more naturally in comparison to an invariant. Hehner [26, 27] strongly
advocates this idea and shows convincing examples. He remarks the expressive
power of summaries as _relations_ between intermediate and final states, a
similar argument is made by Mraihi et al. [44] for invariants. The benefits of
such flexible proof schemas for loops are generally acknowledged [9, 50, 14],
notably in Separation Logic, where tracking the frame is problematic with just
invariants [55, 36, 19, 10]. Yet, invariants are still the predominant
methodology for loop verification.

#### Contribution:

In this paper, we provide a deep investigation of the summary-based approach
in comparison to invariant-based verification, from a theoretical and from an
empirical point of view, leading to several key insights and results.

  * $\bullet$

We formulate summary-based verification (Sec. 3) to clearly exhibit the dual
nature of invariants and summaries, generalizing Hoare’s approach [31] as well
as Hehner and Gravel’s technique for for-loops [27].

  * $\bullet$

We show that summary-based verification is a _complete_ method with respect to
a class of invariants that guarantee safe execution of the body (Thm. 3.4).

  * $\bullet$

We provide _constructive translations_ between the approaches (Props. 1 and 2
in Sec. 4), which not only _explains_ their theoretical parity, but also
provides practical guidelines for building and integrating tools for the two
approaches.

  * $\bullet$

We reify the approach of Tuerk [55] as a standard syntactic Hoare-style proof
rule, based on the insight that the old-keyword and specification statements
(Morgan [43]) can neatly encode an inductive hypothesis (Sec. 5).

To empirically substantiate the claim that summaries are a principled
technique, we implement both approaches in a prototype verifier called Korn.

  * $\bullet$

We evaluate whether state-of-the-art Horn clause solvers [22, 8, 33] are
effective not only in finding invariants but also summaries (Sec. 6), in a
side-by-side comparison on a substantial subset of the SV-COMP benchmarks [5].

The results are promising, given that the algorithms in the backends are
specific to invariants but not to summaries: For example, in category
ReachSafety-Loops, where the performance of the approaches differs most,
Eldarica 2.0.4 solves 117 tasks with invariants in comparison to 112 with
summaries, and Z3 4.8.9 solves 105 vs. 75, respectively (95% resp. 71%). When
giving the freedom to choose between invariants and summaries, Eldarica solves
109 benchmarks and Z3 solves 71. In ReachSafety-ControlFlow, Z3 even finds two
additional proofs using summaries.

Code & Data, Isabelle Proofs: 6cm https://github.com/gernst/korn
Extended Version: 6cm https://arxiv.org/abs/2010.05812

##  2 Motivation and Overview

This section demonstrates the different verification approaches, using
Euclid’s algorithm as an example. The goal is not to argue that summaries are
generally superior to invariants (we think they are complementary). Rather, we
aim to shed light into the ideas and reasoning principles underlying the two
approaches, and into their commonalities and differences. The example is not
chosen for its difficulty or because it works much better with summaries, but
to serve this discussion and to anticipate the formal results in Sects. 3 and
4. Further examples and their discussion can be found in the extended version
of this paper [20].

    assume(x0 > 0);
    assume(y0 > 0);

    unsigned int x = x0;
    unsigned int y = y0;

    while(x != y) {
      if(x > y) x -= y;
      else      y -= x;
    }

    assert(x == gcd(x0,y0));

initially
$x_{0}=\texttt{x0},y_{0}=\texttt{y0}$

forward invariant
$\gcd(\texttt{x0},\texttt{y0})=\gcd(x_{0},y_{0})$
1.6cm $\downarrow$
$\gcd(\texttt{x0},\texttt{y0})=\gcd(x_{1},y_{1})$

1.65cm $\vdots$

$\gcd(\texttt{x0},\texttt{y0})=\gcd(x_{n},y_{n})$

finally
$\texttt{x}=x_{n}=y_{n}=\texttt{y}$

conclusion
$\gcd(\texttt{x0},\texttt{y0})=\underbrace{\gcd(x_{n},y_{n})}_{\stackrel{{\scriptstyle\scalebox{0.7}{\scriptsize
def}}}{{=}}x_{n}}$

finally
$\texttt{x}=x_{n}=y_{n}=\texttt{y}$

backwards summary
$x_{n}=\gcd(x_{n},y_{n})$
1.6cm $\downarrow$
$x_{n}=\gcd(x_{n-1},y_{n-1})$

1.65cm $\vdots$

$x_{n}=\gcd(x_{0},y_{0})$

initially
$x_{0}=\texttt{x0},y_{0}=\texttt{y0}$

conclusion
$x_{n}=\gcd(\texttt{x0},\texttt{y0})$

Figure 1: Euclid’s algorithm and two partial proof sketches for its
correctness. The proof in the middle uses an invariant that propagates
forward, whereas the proof on the right uses a summary that propagates
backwards.

#### Example: Euclid’s Algorithm.

Consider Euclid’s algorithm to compute the greatest common divisor, shown in
Fig. 1. The specification refers to a mathematical function $\gcd$, defined
for arguments $x,y>0$ by the equation

$\displaystyle\gcd(x,y)$ $\displaystyle=\begin{cases}x&x=y\\\
\gcd(x-y,y)&x>y\\\ \gcd(x,y-x)&x<y\end{cases}$

An arbitrary terminating execution of the loop in Fig. 1 with $n$ iterations
can be described using logical variables $x_{i}$ and $y_{i}$ to capture the
state at the beginning of the $i$-th iteration, for $i=0,\ldots,n$, where
$x_{0}=\texttt{x0}$ and $y_{0}=\texttt{y0}$ coincide with the values of the
two program variables initially, each $x_{i+1},y_{i+1}$ is computed from
$x_{i},y_{i}$ with $x_{i}\neq y_{i}$ by unrolling the body once more, and
$x_{n}=y_{n}$ captures the final value. For the remainder of this section, we
freely refer to these variables even though this means that the argument
remains somewhat schematic rather than fully formal. The goal is to prove
$x_{n}=\gcd(x_{0},y_{0})$,

The traditional approach uses an _invariant_
$\gcd(x_{i},y_{i})=\gcd(x_{0},y_{0})$ that relates the current $i$-th state to
the state at loop entry. The core proof step propagates this invariant from
$i$ to $i+1$, as shown in Fig. 1 in the middle. We observe that execution of
the loop body matches the recursive definition of $\gcd$, such that
$\gcd(x_{i},y_{i})=\gcd(x_{i+1},y_{i+1})$, and therefore the invariant holds
in the successor state again, i.e., $\gcd(x_{i+1},y_{i+1})=\gcd(x_{0},y_{0})$
(by transitivity).

The approach promoted in this paper uses a _summary_
$x_{n}=\gcd(x_{i},y_{i})$, which in contrast relates the current $i$-th state
to the _final_ $n$-th state reached at loop exit. Dually to an invariant, this
condition propagates from $i+1$ to $i$ backwards over the completed loop
iterations, as shown in Fig. 1 on the right. The core proof step, again, is to
establish $\gcd(x_{i},y_{i})=\gcd(x_{i+1},y_{i+1})$, but now we conclude
$x_{n}=\gcd(x_{i},y_{i})$ from $x_{n}=\gcd(x_{i+1},y_{i+1})$.

#### Comparison and Key Insights:

When contrasting the invariant and the summary, the latter is not only
smaller, but also conceptually clearer: It succinctly states the intention
behind the algorithm, namely that the loop computes in $x_{n}$ the greatest
common divisor, albeit wrt. an arbitrary initial values of $x_{i}$ and
$y_{i}$, not just $x_{0}$ and $y_{0}$. Acknowledging that the need to
generalize is inherent to induction, we may appreciate that the summary almost
literally occurs in the verification task inside the assertion, which cannot
be said of the invariant.

For both proofs, we additionally need invariants $\texttt{x}>0$ and
$\texttt{y}>0$ omitted so far, so that the applications of the $\gcd$ function
are defined (and to guarantee termination of the algorithm, which we disregard
in this paper). This additional constraint is an instance of a more general
class of invariants, that guarantee “safe” execution of the loop body (see
Def. 3), which cannot be expressed by summaries in the first place. It
reflects an inherent limitation of the backwards reasoning underlying
summaries, to be clarified with Cor. 1. In the following, we therefore
consider an invariant $I$, as a unary predicate on states, together with a
summary $R$, as a relation between an intermediate state and a final one.

$s_{0}$$s_{i}$$s_{i+1}$$s_{n}$body${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}P(s_{0})}\implies{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}I(s_{0})}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}t(s_{i})\land
I(s_{i})}$$\implies{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}I(s_{i+1})}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\lnot
t(s_{n})}\implies{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R(s_{n},s_{n})}$assume
$R(s_{i+1},s_{n})$prove $R(s_{i},s_{n})$finally $P(s_{0})\land
R(s_{0},s_{n})\implies Q(s_{n})$ Figure 2: Forward propagation of an invariant
$I$ and the backward propagation conditions for a summary $R$ with respect to
an iteration of the loop. Assumptions are marked in blue, proof obligations in
red, and the overall conclusion in green.

The reasoning steps in this approach are visualized abstractly in Fig. 2. The
figure shows an arbitrary execution of a loop (in the middle), with
precondition $P$ that is assumed to hold initially in state $s_{0}$, and with
postcondition $Q$, which we aim to prove in state $s_{n}$. At the top of the
figure, the usual initialization and forward propagation conditions for an
invariant $I$ are shown wrt. an arbitrary iteration of the loop body from
state $s_{i}$ to $s_{i+1}$.

The summary $R$, in contrast, is intended to approximate the _remaining_
iterations until loop exit. As such, it is established in state $s_{n}$ from
$t(s_{n})$ to hold reflexively as $R(s_{n},s_{n})$, which intuitively means
that $R$ is adequate for zero iterations. The first argument of $R$, which
references the starting point, must then propagate backwards over any step of
the loop, i.e., we may assume $R(s_{i+1},s_{n})$ to prove $R(s_{i},s_{n})$,
which intuitively means that as long as $R$ adequately describes the remaining
iterations, this particular leading execution of the loop body can be included
in the summary, too. As a consequence, the _entire_ loop is represented by
$R$, which together with the precondition implies the postcondition.

Neither invariant $I$, nor negative loop test $\lnot t$ occur in that proof
obligation to establish postcondition $Q$. Both can be represented as part of
$R$: In the absence of break we may choose the summary such that
$R(s,s_{n})\implies\lnot t(s_{n})$ holds. Similarly, we may qualify the
summary with respect to the invariant (cf. Prop. 2).

At a more fundamental level, summaries generalize and give an explicit handle
on the conclusion of the underlying induction proof. Schematically, in Hoare’s
approach, the loop will lead to a final state $s_{n}$ where the invariant
holds, as well as the negated loop test, which instantiates the conclusion in
a predetermined way. Summaries recover precisely this parameter of the proof
and give control over its instantiation. Informally, we therefore make use of
the respective
Induction principles: with invariants (Thm. 3.1) with summaries (Thm. 3.3)
$I(s_{i})~{}\rightsquigarrow~{}I(s_{n})\land\lnot t(s_{n})$
$I(s_{i})~{}\rightsquigarrow~{}R(s_{i},s_{n})$

stepping from $i$ to $i+1$, where $\rightsquigarrow$ denotes the remaining
iterations of the loop.

#### Syntactic Specifications:

Recall that when expressing the invariant and the summary, we referred to the
logical variables which were introduced solely for the discussion. We can
represent the invariant directly as
$\gcd(\texttt{x},\texttt{y})=\gcd(\texttt{x0},\texttt{y0})$ in terms of the
variables occurring in the program. Alternatively, we can use the old keyword
to specify
$\gcd(\texttt{x},\texttt{y})=\gcd(\texttt{old}(\texttt{x}),\texttt{old}(\texttt{y}))$,
but we do not _need_ to, as auxiliary variables can always be introduced into
the program for that purpose.

For the summary, however, where $x_{n}$ has no counterpart in the program and
it is unclear how to introduce one, the old keyword (or a similar mechanism)
becomes an essential tool to specify the relation that describes the execution
of the loop. We thus encode the summary as
$\texttt{x}=\gcd(\texttt{old}(\texttt{x}),\texttt{old}(\texttt{y}))$, where
the plain occurrence of variable x refers to the final state, and old marks
the occurrences that move backwards over iterations. With this representation,
we can see clearly how the summary generalizes assertion x == gcd(x0,y0) in
Fig. 1.

In the following, we use notation $a[i..j]$, which constructs a mathematical
sequence from array $a$ containing the elements $a[i],\ldots,a[j-1]$ wrt.
inclusive lower bound $i$ and exclusive upper bound $j$ to simplify the
presentation. We abbreviate $x\in a\iff\exists\ k.\ a[k]=x$ for a valid index
$k$.

#### Example: Linear Search.

The following program determines in $r$ if element $x$ occurs in array $a$
with length $n$.
int i=0; bool r=false; while(!r && i<n) r = (x == a[i]); i++;
We aim to prove that finally $r\iff x\in a[0..n]$, and note that the
interesting case is when $x$ is not found. A correct invariant that entails
the postcondition in that case is $x\not\in a[0..i]$, which generalizes the
upper bound of the slice. A correct summary omits the negation, generalizes
the lower bound, and also the starting value of $r$ (needed for the base case
of loop exit when the last iteration has set $r$ to $\mathit{true}$):
$r\iff\texttt{old}(r)\lor a[\texttt{old}(i)..n]$.

#### Example: Array Copy.

This example copies $n$ elements from array $a$ to $b$:
int i=0; while(i<n) b[i] = a[i]; i++;
We aim to prove that finally $b[0..n]=a[0..n]$. Given loop counter $0\leq
i\leq n$, the key part of the invariant is $b[0..i]=a[0..i]$, but we do not
need to constrain $b[i..]$.

A sufficiently strong summary needs to be explicit about the final value of
$i$ and the contents of the _entire_ resulting array $b$. Interpreted in the
final state we have summary $i=n\land
b=\texttt{old}(b)[0..\texttt{old}(i)]\circ a[\texttt{old}(i)..n]$ where
$\circ$ is subrange concatenation, and recall that old refers to an arbitrary
intermediate state in the inductive step. Intuitively, the additional round-
trip to the loop exit means that we “forget” the fact that the prefix has been
copied already. In other words, the summary must be stronger in some sense
than the invariant here, albeit we think that using a precise framing
mechanism could address the problem, see e.g. [45], so that summary $i=n\land
b[\texttt{old}(i)..n)=a[\texttt{old}(i)..n]$ would suffice.

#### Example: Phone Number Comparison.

In last example, communicated by Rustan Leino, emphasizes the advantage of
summaries nicely. Consider the comparison of phone numbers after filtering out
additional characters such as dashes, parentheses, and whitespace. As an
example, the phone numbers (01) 23 45 and 01-2345 should be regarded the same,
whereas 1-23-45 is different because of the missing leading 0.

The approach in question keeps two indices, $j$ and $k$, into arrays $a$ and
$b$, which store the characters of the respective numbers. The algorithm
consists of a loop that increments $j$ if $a[j]$ is not a digit, similarly for
$k$ and $b[k]$, terminates with a negative result $r=\mathit{false}$ if two
digits $a[j]\neq b[k]$ and proceeds otherwise till one of the arrays is
exhausted, setting $r$ to true of the other array is exhausted, too. The
algorithm is correct, if
$r\Leftrightarrow\texttt{filter}(X,a[0..a.\texttt{length}])=\texttt{filter}(X,b[0..b.\texttt{length}])$
where $X$ is the characters to keep, where filter is defined over a sequence
of values by recursion:

$\displaystyle\texttt{filter}(X,[])$ $\displaystyle=[]$
$\displaystyle\texttt{filter}(X,\texttt{cons}(h,t))$
$\displaystyle=\begin{cases}\texttt{filter}(X,t),h\in X\\\
\texttt{cons}(h,\texttt{filter}(X,t)),\text{otherwise}\end{cases}$

The corresponding summary simply generalizes constant $0$ from the
postcondition to $\texttt{old}(i)$. The most obvious invariant involves
$\texttt{filter}(X,a[0..j])=\texttt{filter}(X,b[..k])$. However, noting that
filter unwinds the first element, but the loop actually discerns some element
in the middle of the sequence, we will need a helper lemma that unfolds filter
at the end. We can avoid this lemma using an alternative invariant instead

$\displaystyle\texttt{filter}(X,a[0..a.\texttt{length}])=\texttt{filter}(X,b[0..b.\texttt{length}])$
$\displaystyle{}\iff$
$\displaystyle\texttt{filter}(X,a[j..a.\texttt{length}])=\texttt{filter}(X,b[k..b.\texttt{length}])$

which states that both phone numbers are the same exactly if the remaining
comparison will determine them to be the same. This invariant then coincides
with the structure of the computation without the need for a lemma.

Observe that this invariant compares the postcondition _to the summary_ , a
pattern that we have seen already with the greatest common divisor. It turns
out that this idea exhibits a fundamental connection between invariants and
summaries, as formalized in Prop. 1.

#### Outlook:

We speculate that there are more—and more fundamental—insights to be gained:
Invariants follow the computation and therefore are potentially better
described in terms of implementation data structures (i.e., those occurring in
the program). Conversely, summaries wrap up a result, which by our experience
is often done by auxiliary mathematical functions that abstract the
implementation data type to a logical counterpart (e.g., linked lists to
sequences [55], linked trees to algebraic trees [19]). Notably, when using
lists, such formulations tend to be right folds (as with filter), whereas a
loop is clearly a left fold, causing the described mismatch wrt. the
invariant, but naturally following backwards alongside the summary.
Fundamentally, invariants as a safety property could be regarded to relate
more closely to coinduction than to induction, whereas summaries rather
coincide with the latter; given that computation can be described as a
coalgebra, whereas observations are expressed by an algebra. We leave this
thought for future work.

##  3 Verification of Loops with Invariants and Summaries

This section succinctly states the approach to the verification with
invariants and loop summaries and with soundness and completeness theorems.
The results have been mechanized in Isabelle/HOL [47]. The presentation here
is based on systems of cyclic Horn clauses, where invariants and summaries are
unknown predicate variables. Alongside each result we point out the practical
consequences for tool use and construction, and we discuss possible variations
in the formalization.

###  3.1 Preliminaries

We consider imperative commands $C$, defined over a semantic domain of states
$S$, as relations $C\subseteq S\times\hat{S}$ with
$\hat{S}=S\uplus\\{\lightning\\}\uplus\\{{s}_{\downarrow}\mid s\in S\\}$,
where $\lightning$ signifies a runtime error, and ${s}_{\downarrow}$ signifies
early exit of a loop via a break command in state $s$. By notational
convention $\hat{s}\in\hat{S}$, whereas $s\in S$ strictly. We use suggestive
naming as in Sec. 2, e.g. state $s_{0}\in S$ is used for the initial state of
some execution, $s,s^{\prime},s^{\prime\prime}$ are intermediate states, and
$s_{n}$ typically refers to a final state of the loop.

######  Definition 1 (Validity of Hoare-Triples)

A command $C\subseteq S\times\hat{S}$ is correct with respect to a
precondition $P\subseteq S$ and a postcondition $Q\subseteq S$, if the Hoare
triple $\\{\,P\,\\}\,C\,\\{\,Q\,\\}$ is valid, written
$\models\\{\,P\,\\}\,C\,\\{\,Q\,\\}$ and defined as usual

$\models\\{\,P\,\\}\,C\,\\{\,Q\,\\}\iff\big{(}\forall s,\hat{s}^{\prime}.\
P(s)\land C(s,\hat{s}^{\prime})\implies Q(\hat{s}^{\prime})\big{)}.$

Note that the domain $S$ of relation $Q$ as a regular state forces
$\hat{s}^{\prime}\in S$ and thus $\hat{s}\neq\lightning$, such that error
outcomes and breaks outside of loops are ruled out as desired. We omit the
treatment of non-termination, as it is orthogonal.

######  Definition 2 (Semantics of Loops)

The semantics of a loop $W(t,B)\subseteq S\times\hat{S}$ with test $t\in S$
and body $B\subseteq S\times\hat{S}$ is the least fixpoint of

$\displaystyle\lnot t(s)$ $\displaystyle\implies W(t,B)(s,s)$ $\displaystyle
t(s)\land B(s,\lightning)$ $\displaystyle\implies W(t,B)(s,\lightning)$
$\displaystyle t(s)\land B(s,{s}_{\downarrow}^{\prime})$
$\displaystyle\implies W(t,B)(s,s^{\prime})$ $\displaystyle t(s)\land
B(s,s^{\prime})\land W(t,B)(s^{\prime},\hat{s}^{\prime\prime})$
$\displaystyle\implies W(t,B)(s,\hat{s}^{\prime\prime})$

The first condition terminates the loop, the second condition propagates
errors in the body, the third condition propagates early loop exit, and the
last condition unrolls the loop once if the first iteration results in a
regular state $s^{\prime}\in S$.

In the following we are concerned in verifying correctness of a loop $W(t,B)$
wrt. precondition $P$ and postcondition $Q$, as expressed by
$\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$.

###  3.2 Loop Invariants

We briefly summarize the relevant ideas and results of Hoare [31] in our
notation.

######  Definition 3 (Loop Invariant)

Predicate $I\subseteq S$ is an inductive _invariant_ of loop $W(t,B)$ wrt. a
precondition $P\subseteq S$, if

$\displaystyle P(s_{0})$ $\displaystyle\implies I(s_{0})$ $\displaystyle
I(s)\land t(s)\land B(s,s^{\prime})$ $\displaystyle\implies I(s^{\prime})$

A loop invariant $I$ is _safe_ wrt. executions of the loop body $B$, if
additionally

$\displaystyle I(s)\land t(s)\land B(s,\lightning)$
$\displaystyle\implies\mathit{false}$

A safe loop invariant $I$ is _correct_ wrt. a postcondition $Q\subseteq S$, if
additionally

$\displaystyle I(s)\land t(s)\land B(s,{s_{n}}_{\downarrow})$
$\displaystyle\implies Q(s_{n})$ $\displaystyle I(s_{n})\land\lnot t(s_{n})$
$\displaystyle\implies Q(s_{n})$

The first condition establishes $I$ initially and the second condition
propagates $I$ over a single iteration of the body otherwise (when
$s^{\prime}\in S$). The third condition prevents errors in the body. The
fourth condition ensures $Q$ after a break directly, and final condition
ensures $Q$ upon regular termination of the loop.

######  Theorem 3.1 (Soundness of Loop Invariants)

Given a correct loop invariant $I$ for a loop $W(t,B)$ with respect to
precondition $P$ and postcondition $Q$, then
$\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$ holds.

###### Proof

We prove $\forall\ s,\hat{s}.\ I(s)\land W(t,B)(s,\hat{s})\implies Q(\hat{s})$
by induction over the least fixpoint of Def. 2, from which the claim follows
by Def. 1. $\square$

######  Theorem 3.2 (Completeness of Loop Invariants)

Given a valid triple,
$\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$, then there exists a corresponding
correct invariant.

###### Proof

Predicate $\lambda s.\ \exists s_{0}.\ P(s_{0})\land I^{*}(s_{0},s)$ is a
correct invariant (Def. 3), where $I^{*}\subseteq S\times S$ is the strongest
relation that characterizes regularly terminating loop iterations, defined as
the least fixpoint of: $\square$

$\displaystyle\lnot t(s)$ $\displaystyle\implies I^{*}(s,s)$ $\displaystyle
t(s)\land B(s,s^{\prime})\land I^{*}(s^{\prime},s^{\prime\prime})$
$\displaystyle\implies I^{*}(s,s^{\prime\prime})$

The result states that all critical pieces of information (e.g. outcome of
loop test $t$) and key reasoning features from the underlying induction proof
are reflected somehow in the constraints of Def. 3. Of course, reasoning about
$I^{*}$ is by no means easier than a proof using the semantic definition, and
the challenge in practice is to find closed-form solutions instead that can be
expressed with functions and predicates given in the background theory.

###  3.3 Loop Summaries

As outlined, a summary is a binary relation $R\subseteq S\times S$, such that
$W(t,B)(s_{0},s_{n})$ implies $R(s_{0},s_{n})$. However, the first argument of
$R$ must be flexible to move across loop iterations, i.e., $R(s,s_{n})$ holds
between all pairs of some intermediate state $s$ and some final state $s_{n}$.
The difference to invariants is that $s$ moves backwards in the proof
obligations. The approach mirrors that of Hehner and Gravel [27, Rules F and
G] for for-loops, however, this presentation does not depend on predicates
indexed by counters and is therefore fully general.

######  Definition 4 (Loop Summary)

$R\subseteq S\times S$ is a _summary_ of $W(t,B)$, if

$\displaystyle\lnot t(s_{n})$ $\displaystyle\implies R(s_{n},s_{n})$
$\displaystyle t(s)\land B(s,{s_{n}}_{\downarrow})$ $\displaystyle\implies
R(s,{s_{n}})$ $\displaystyle t(s)\land B(s,s^{\prime})\land
R(s^{\prime},s_{n})$ $\displaystyle\implies R(s,s_{n})$

A summary is _correct_ wrt. a precondition $P$ and a postcondition $Q$, if
also

$\displaystyle\hskip 33.28966ptP(s_{0})\land R(s_{0},s_{n})$
$\displaystyle\implies Q(s_{n})$

The first condition establishes that $R$ holds reflexively at a regular loop
exit. The second line establishes that $R$ summarizes the last partial
execution of the loop body when a break is encountered. The third line lifts a
summary of some remaining iterations until termination of the loop to a
summary that accounts for an additional leading iteration. Note that if an
invariant $I$ is known, it can be assumed for states $s$ above, but Thm. 3.4
shows that we don’t need to. The last line applies the summary $R$ to the
original pre-state $s_{0}$ that satisfies $P$ to establish the postcondition
$Q$. The inclusion of $P(s_{0})$ will be necessary for Thm. 3.4.

######  Theorem 3.3 (Soundness of Loop Summaries)

Given a _safe_ loop invariant $I$ and a _correct_ summary $R$ for a loop
$W(t,B)$ wrt. precondition $P$ and postcondition $Q$, then
$\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$ holds.

###### Proof

We prove $\forall\ s,\hat{s}.\ I(s)\land W(t,B)(s,\hat{s})\implies
R(s,\hat{s})$ by induction over the least fixpoint of Def. 2, from which the
claim follows by Def. 1. $\square$

As mentioned, it is possible to strengthen Def. 4 by including any invariant
as additional premises in the first three conditions, however, it is neither
known that $\lnot t(s_{n})$ in the fourth condition that summarizes the entire
loop, due to break, as in Def. 3. Similarly, we cannot assume such an
invariant as $I(s_{n})$ there. While exploiting additional invariants is
clearly desirable in practice, we prefer to keep the presentation minimal, as
the approach is still complete without explicit reference to invariants in
Def. 4.

######  Theorem 3.4 (Completeness of Loop Summaries wrt. Safe Invariants)

Given a valid triple, $\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$ and $I$ is a
safe invariant for this loop, then there exists a corresponding correct
summary $R$.

###### Proof

The desired summary $R^{*}\subseteq S\times S$ is the least fixpoint of

$\displaystyle\lnot t(s)$ $\displaystyle\implies R^{*}(s,s)$ $\displaystyle
R^{*}(s_{0},s)\land t(s)\land B(s,{s}_{\downarrow}^{\prime})$
$\displaystyle\implies R^{*}(s_{0},s^{\prime})$ $\displaystyle t(s)\land
B(s,s^{\prime})\land R^{*}(s^{\prime},s^{\prime\prime})$
$\displaystyle\implies R^{*}(s,s^{\prime\prime})$

which is the strongest relation that characterizes terminating loop
iterations, possibly ending with a break command (in contrast to $I^{*}$ of
Thm. 3.2).

We rely on the presence of $P(s_{0})$ in the last condition of Def. 4:
$R^{*}(s_{0},s_{n})$ implies $W(t,B)(s_{0},s_{n})$, which proves $Q(s_{n})$
via validity of the Hoare triple.111Explicitly including $P(s_{0})$ in the
last condition of Def. 4 seems not strictly necessary, as presumably this fact
can be made part of $I(s_{0},s)$ and thus the summary shown to exist can claim
$\exists\ s_{0}.\ P(s_{0})\land I(s_{0},s)$ in addition to $R^{*}(s,s_{n})$.
However, the chosen presentation fits better with the mechanization, where
otherwise the extra existential quantifier is cumbersome to deal with.
$\square$

Conceptually, this decomposition using a safe invariant and a summary
resembles the decomposition of total correctness into termination and partial
correctness.

##  4 Bridging Between the Approaches

Having soundness and completeness of both approaches we characterize their
relationship. Safe execution of the loop body turns out to be precisely the
condition that needs to propagate forwards and cannot be covered by summaries.

######  Corollary 1 (Safe Invariants are Necessary and Sufficient)

Given a semantically correct loop, $\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$.
There exists a summary $R$ iff there exists a safe invariant $I$.

###### Proof

From the completeness of the two approaches, Thms. 3.2 and 3.4. $\square$

As a consequence, both methodologies are equivalent in the following sense:

######  Corollary 2 (Coincidence of Invariants and Summaries)

Given a loop $W(t,B)$ with precondition $P$ and postcondition $Q$. There
exists a corresponding correct invariant $I$ iff there exists a safe invariant
$J$ and a correct summary $R$.

###### Proof

In both directions, we have $\models\\{\,P\,\\}\,W(t,B)\,\\{\,Q\,\\}$ by Thms.
3.1 and 3.3, respectively, the claim then follows by Cor. 1. $\square$

These corollaries should not be surprising, but the proof via the completeness
theorems and the underlying constructions $I^{*}$ and $R^{*}$ is
unsatisfactory. A direct translation that avoids these artifacts is clearly
more useful, by constructing $I$ from $J$ and $R$, and vice-versa, $R$ from
$I$ and $Q$, as shown with Props. 1 and 2. Not only does it give a direct and
obvious proof of Cor. 2, but both results have immediate practical use as
discussed subsequently.

######  Proposition 1 (Lifting of Summaries to Invariants)

Given a pair of a safe invariant $J$ and a correct summary $R$, then $I$ is a
correct invariant, where

$\displaystyle I(s)~{}\coloneqq~{}\exists\ s_{0}.\ P(s_{0})\land
J(s)\land\big{(}\forall\ s_{n}.\ R(s,s_{n})\implies R(s_{0},s_{n})\big{)}$ (1)

The first conjunct keeps track of the existence of some initial state $s_{0}$
that satisifies $P$, which is needed to make use of the correctness condition
of $R$ in Def. 4. The second conjunct includes $J$ to establish safe execution
of the loop body. The third conjunct predicts that a summary of the remaining
iterations wrt. current state $s$ and an arbitrary final state $s_{n}$ can be
lifted to a summary of the whole loop execution beginning at $s_{0}$.

######  Proof (of Prop. 1)

We have to show all conditions of Def. 3 for the lifted invariant (1).
Initialization from a given $P(s_{0})$ is trivial by choosing the existential
quantifier as that state. For the rest of the proof we may assume $P(s_{0})$
for an arbitrary $s_{0}$. For propagation of the invariant over a regular
iteration $t(s)\land B(s,s^{\prime})$ of the body, the key observation is that
$\forall\ s_{n}.\ R(s^{\prime},s_{n})\implies R(s_{0},s_{n})$ follows from
$\forall\ s_{n}.\ R(s,s_{n})\implies R(s_{0},s_{n})$ for the same $s_{0}$ and
$s_{n}$, as $R(s^{\prime},s_{n})$ implies $R(s,s_{n})$ via Def. 4. When
exiting the loop via break in state ${s_{n}}_{\downarrow}$, from Def. 4 we
have $R(s,s_{n})$, which by the third conjunct of (1) provides summary
$R(s_{0},s_{n})$ of the entire execution. Together with $P(s_{0})$ this
implies $Q(s_{n})$ by correctness of $R$. Regular loop exit with $\lnot
t(s_{n})$ is analogous. $\square$

Prop. 1 effectively means that summaries can be supported easily in the
frontend of a deductive verifier like Dafny [40] that takes specifications
from the user. Given the translation above, the only necessary extensions are
adding summary annotations to loops and expressing relational predicates, e.g.
using the old keyword. Even without such support, the result provides a
guideline to craft such annotations with a manual encoding.

One might worry about the of additional quantifiers. When verification
conditions are path-sensitive (e.g. in wp-calculus or symbolic execution),
then $P(s_{0})$ can be kept in context for a fixed $s_{0}$ by default.
Moreover, as in the examples of Sec. 2, when $R(s,s_{n})$ is an equation of
the form $s_{n}=f(s)$, then the third conjunct collapses to $f(s)=f(s_{0})$
and the universal quantifier can be dropped.

The analogue of (1) is useful in Separation Logic [49], too. Simply by using
spatial operators $*$ and $-*$ instead of their propositional counterparts, we
obtain

$\displaystyle I(s)~{}\coloneqq~{}\exists\ s_{0}.\
P(s_{0})*J(s)*\big{(}\forall\ s_{n}.\
R(s,s_{n})\mathrel{-*}R(s_{0},s_{n})\big{)}$ (2)

which has been noted in a similar form in [53] as an encoding of Tuerk’s
approach [55], but [53] is not explicit about which states are referenced and
it uses a non-relational postcondition instead.

Conversely to Prop. 1, a tool with first-class support for summaries can be
turned into a purely invariant-based verifier. The gap between the conditions
of Def. 3 and Def. 4 wrt. postcondition $Q$ can be closed by canonical
summaries:

######  Proposition 2 (Lifting of Postconditions to Summaries)

$I$ is a correct invariant iff $I$ is a safe invariant and $R$ is a correct
summary, where

$\displaystyle R(s,s_{n})~{}\coloneqq~{}I(s)\implies Q(s_{n})$ (3)

###### Proof

Matching case by case of Defs. 3 and 4, noting, slightly amused, that the
backwards propagation condition in Def. 4 becomes trivial. The cases for
regular termination and break of the summary follow from those of the correct
invariant only because the missing premise $I(s_{n})$ is injected via (3).
$\square$

#### Combined Approach.

We briefly show the combined approach that simply collects all verification
conditions and assumes the invariant for backwards propagation of the summary:

$\displaystyle P(s_{0})$ $\displaystyle\implies I(s_{0})$ $\displaystyle
I(s)\land t(s)\land B(s,s^{\prime})$ $\displaystyle\implies I(s^{\prime})$
$\displaystyle I(s)\land t(s)\land B(s,\lightning)$
$\displaystyle\implies\mathit{false}$ $\displaystyle I(s_{n})\land\lnot
t(s_{n})$ $\displaystyle\implies R(s_{n},s_{n})$ $\displaystyle I(s_{n})\land
t(s)\land B(s,{s_{n}}_{\downarrow})$ $\displaystyle\implies R(s,{s_{n}})$
$\displaystyle I(s)\land t(s)\land B(s,s^{\prime})\land R(s^{\prime},s_{n})$
$\displaystyle\implies R(s,s_{n})$ $\displaystyle P(s_{0})\land
R(s_{0},s_{n})$ $\displaystyle\implies Q(s_{n})$

######  Proposition 3 (Coincidence of the Combined Approach)

The above verification conditions are exactly equivalent to stating that $I$
is a safe invariant and that canonical summary $\lambda\ s,s_{n}.\
I(s)\implies Q(s_{n})$ is correct.

This formulation underlies configuration 3. in Sec. 6. It is moreover the most
useful formulation for interactive tools, i.e., when invariants and summaries
are specified by the user, and the strongest assumptions possible are desired.

##  5 Summaries in Hoare Logic

In this section we present a Hoare logic proof rule for the verification of
loops with invariants and summaries. The result mirros that of Tuerk [55] in
the context of Separation Logic, however, he uses a shallow embedding of
formulas, programs, and Hoare triples in the higher-order logic of the HOL
system. The inductive case for one iteration of the body $B$ with test $t$ is
expressed in [55] as

$\displaystyle\forall\ x,C.\ \big{(}\forall\ y.\
\\{\,P(y)\,\\}\,C\,\\{\,Q(y)\,\\}\big{)}\implies\\{\,t(x)\land
P(x)\,\\}\,B;C\,\\{\,Q(x)\,\\}$ (4)

where the premise of the implication amounts to the inductive hypothesis for
the remaining loop iterations, abstracted here by arbitrary the command $C$.

It is not immediate how Tuerk’s approach can be reified in a traditional form,
such that it avoids escaping to the meta-level with Hoare triples as first-
class objects. The primary question is how to represent the inductive
hypothesis, and our key insight is that _specification statements_ (Morgan
[43]) together with old-references lead to an elegant formulation as rule
Summary below. Although not presented here, the approach works equivalently
with predicate transformers, see Alexandru’s bachelor thesis [2] for a
comprehensive account.

###  5.1 Preliminaries

To this end, we make the distinction between syntax and semantics more
precise: Predicates $P,Q,I,R$ are represented as formulas in this section.
These may refer to variables $x$, $y$ and can be evaluated in states $s$ as
$\llbracket{P}\rrbracket(s)\in\mathbb{B}$. By $P[x\mapsto y]$ we denote the
renaming of $x$ to $y$ in $P$, and by convention we overline vectors of
variables $\overline{x}$. Derivability of Hoare triples is written
$\vdash\\{\,P\,\\}\,C\,\\{\,Q\,\\}$. We omit the treatment of break for
simplicity, see e.g. [34].

A specification statement $\overline{x}\colon[P,Q]$ defines a precondition
$P$, a set of variables $\overline{x}$ that are nondeterministically modified,
and a relational postcondition $Q$ that constrains the transition. Within $Q$,
the previous values of variables $\overline{x}$ can be referred to the
syntactic form $\texttt{old}(x)$, well-known from its use in invariants and
method postconditions (e.g. [40]).

Specification statements generalize the widely used statements for assertions
$P$, assumptions $Q$ (not using old), and havocing of variables (where
$\langle\rangle$ denotes an empty vector of variables), as used in e.g. Boogie
[39].

$\displaystyle\texttt{assert}~{}P$
$\displaystyle\equiv\langle\rangle\colon[P,\mathit{true}]$
$\displaystyle\texttt{assume}~{}Q$
$\displaystyle\equiv\langle\rangle\colon[\mathit{true},Q]$
$\displaystyle\texttt{havoc}~{}\overline{x}$
$\displaystyle\equiv\overline{x}\colon[\mathit{true},\mathit{true}]$

The built-in provision for old in comparison to a combination of the three
distinct statements will be convenient later on.

######  Definition 5 (Semantics: Specification Statement)

The semantics of a specification statement
$\llbracket{xs\colon[P,Q]}\rrbracket$ is the smallest relation satisfying:

$\displaystyle\lnot\llbracket{P}\rrbracket(s)$
$\displaystyle\implies\llbracket{\overline{x}\colon[P,Q]}\rrbracket(s,\lightning)$
$\displaystyle\llbracket{P}\rrbracket(s)\land
s^{\prime}=s(\overline{x}\mapsto\overline{a})\land\llbracket{Q}\rrbracket(s,s^{\prime})$
$\displaystyle\implies\llbracket{\overline{x}\colon[P,Q]}\rrbracket(s,s^{\prime})$

The first line results in an error successor state $\lightning$ if the
precondition is violated. Otherwise, in the second line, we introduce a new
successor state $s^{\prime}$ that differs from $s$ in the values
$\overline{a}$ for the modified variables $\overline{x}$, such that the
transition predicate $Q$ is satisfied. The bare-bone proof rule for the
specification statement is

$\displaystyle\vdash\\{\,P\,\\}\,~{}\overline{x}\colon[P,Q]~{}\,\\{\,Q[\texttt{old}(\overline{x})\mapsto\overline{x}_{0}]\,\\}\overline{x}_{0}\text{
fresh}$

which requires precondition $P$ and establishes postcondition $Q$ with fresh
logical variables $\overline{x}_{0}$ in place of the
$\texttt{old}(\overline{x})$. For convenience, the proof rule can be modified
to include $P[\overline{x}\mapsto\overline{x}_{0}]$ in the postcondition,
alternatively one can just specify this information as part of $Q$ using old.

###  5.2 Proof Rule for Summaries

The proof rule to verify a loop $\texttt{while}\ t\ \texttt{do}\ B$ with test
$t$ and body $B$ is show below. The variables $\overline{x}=\text{mod}(B)$ are
those modified by body $B$, whereas $\overline{x}_{0}$, $\overline{x}_{i}$,
$\overline{x}_{n}$ are fresh logical variables capturing various intermediate
states.

$\displaystyle\vdash\\{\,P\land\overline{x}=\overline{x}_{0}\,\\}\,~{}\texttt{while}\
t\ \texttt{do}\
B~{}\,\\{\,Q[\texttt{old}(\overline{x})\mapsto\overline{x}_{0}]\,\\}\begin{array}[]{c}\vdash\\{\,P\,\\}\,~{}\overline{x}\colon[I,R]~{}\,\\{\,Q\,\\}\\\\[2.0pt]
\vdash\\{\,I\land\lnot
t\land\overline{x}=\overline{x}_{n}\,\\}\,~{}\texttt{skip}~{}\,\\{\,R[\texttt{old}(\overline{x})\mapsto\overline{x}_{n}]\,\\}\\\\[2.0pt]
\vdash\\{\,I\land t\land\overline{x}=\overline{x}_{i}\,\\}\,~{}B;\
\overline{x}\colon[I,R]~{}\,\\{\,R[\texttt{old}(\overline{x})\mapsto\overline{x}_{i}]\,\\}\end{array}$

The first premise summarizes computation of the entire loop by $I$ and $R$
using a specification statement. From rule Spec, proof obligations akin to
those in Def. 4 are immediate via an application of the consequence rule.

The second premise terminates the loop when $\lnot t$, the variables
$\overline{x}_{n}$ capture this final state. We encode the corresponding proof
obligation as a Hoare triple with command skip,222Tuerk [55] remarks that,
more generally, the inductive hypothesis may encompass a subsequent program
fragment $C$ right after the loop, i.e., $\texttt{while}\ t\ \texttt{do}\
B;C$, and this (concrete) $C$ would then replace skip in the second premise,
with $\overline{x}=\textrm{mod}(B,C)$. th which is equivalent to $I\land\lnot
t\implies R[\texttt{old}(\overline{x})\mapsto\overline{x}]$, mirroring the
exit condition from Def. 4.

In the third premise, in contrast to [55], the inductive hypothesis is
directly embedded into the program as specification statement
$\overline{x}\colon[I,R]$ that summarizes the remaining iterations after
executing $B$ once. The variables $\overline{x}_{i}$ in the precondition of
the triple capture the state right before $B$ is executed for later reference
in the postcondition, whereas the old-reference to the intermediate state
after $B$, needed for $R$ in $\overline{x}\colon[I,R]$, is handled implictly
via rule Spec. Hence, the rule nicely retains the syntax-oriented,
compositional nature of Hoare’s approach.

To understand the third premise, it is useful to visualize the symbolic
computation and reasoning steps involved:

$\overline{x}_{i}$$B$$\overline{x}\colon[I,R]$$I\land
t$$\implies{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}I}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}R[\texttt{old}(x)\mapsto\overline{x}_{i+1}]}\implies{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}R[\texttt{old}(x)\mapsto\overline{x}_{i}]}$$\overline{x}\colon[I,R]$

Initially, for $\overline{x}=\overline{x}_{i}$ we assume $I\land t$. The body
$B$ transitions to some successor state (depicted as a hollow circle), where
we have to re-establish the invariant as the premise for rule Spec. This rule
introduces a fresh variable, suggestively named $\overline{x}_{i+1}$ here, to
capture this intermediate state, which then gets substituted in place of old
to obtain a summary of the remaining iterations. Per consequence, we then need
to establish postcondition
$R[\texttt{old}(\overline{x})\mapsto\overline{x}_{i}]$ of the Hoare triple in
the third premise of rule Summary, as depicted below the final state (solid
circle), mirroring the backwards propagation condition from Def. 4. Overall,
this justified to approximate the entire loop by $\overline{x}\colon[I,R]$.

##  6 Evaluation with Horn Clause Solvers

This evaluation considers whether state-of-the-art solvers for systems of Horn
clauses can be used to infer summaries automatically. The benchmark set of the
yearly CHC competition [51]333https://github.com/chc-comp/chc-
comp20-benchmarks contains verification tasks that are based on invariants
only, and consequentially, one might assume that the implemented techniques
are geared towards the shape of the resulting verification conditions.

#### Research Question:

_Can we automate the approach in practice, i.e., can existing solvers
instantiate not only invariants but also summaries?_

It will be of particular interest, whether correctness can be encoded
primarily into summaries, relying on safe invariants only. This will an
experimental account of whether completeness, as stated in Thm. 3.4, can
actually be relied on.

The evaluation is based on a prototype tool, described below, that implements
both invariants and summaries, such that a fair comparison between the
different approaches is ensured. As benchmark, we consider all currently
supported tasks of selected categories of the SV-COMP
repository,444https://github.com/sosy-lab/sv-benchmarks where the goal is to
prove correctness, encoded as the unreachability of a specific function.

It is not a primarly goal to improve the overall performance over the state-
of-the-art [5] across a wide range of benchmarks, as it would require
significant additional engineering effort to support all the C features
present in the SV-COMP benchmarks. The results are shown in Table 1 and Fig.
3.

#### Implementation

We have implemented the approach as a prototype tool called Korn. It reads C
source files and translates them into a system of Horn clauses that can be
instantiated by off-the-shelf solvers. Code and setup are
public.555https://github.com/gernst/korn, using /commit/91132f for the
evaluation.

The translation from C to Horn clauses abstracts all basic blocks in the
program as predicates for which the solver has to find a solution. In contrast
to the encoding outlined in [8], we collapse straight-line code into a single
predicate using symbolic execution, reducing the number of predicates for ease
of solving and ease of debugging the generated verification task. Predicates
are introduced notably for invariants, summaries, at join points after a
conditional, and at labels. Moreover, each function is represented by a
precondition predicate over the input parameters, and a summary that
additionally refers to the return value.

For the invariant-based approach, it is sufficient to let these predicates
range over single states. However, using summaries mandates a translation that
keeps track of the origin of a computation, hence all predicates, except
function pre- and postconditions, are encoding _transitions_ , with two sets
of state variables.

The implementation currently suffers from a few limitations, which means that
in each category considered, only a subset of the tasks is supported (cf.
Table 1), nevertheless, we are able to obtain a substantial number of results.
Specifically, arrays are treated as value types without bounds, and there is
no model of the heap currently, which is unsound but sufficient as a work-
around in most cases. Other unsupported features include: global variables,
array initializers, dynamic memory allocation (malloc/free), floating point
numbers, structs and unions, and finally assignments from array variables to
pointers. Unstructured control flow with goto and return is supported, though,
as it is rather straight-forward in the Horn clause based encoding.

#### Experimental Setup

We focus on four categories from the SV-COMP benchmark repository, Arrays,
Loops, Recursion, and ControlFlow,666The recently added benchmarks in nla-
digbench-scaling were not considered, these are variants of other benchmarks
that were evaluated, but with explicit bounds. where 459 of a total of 925
benchmarks are currently supported by Korn. All from the class ReachSafety,
i.e., the question whether a special function reach_error is called on any of
the execution paths. These benchmarks contain nondeterministic choice in terms
of designated functions, as well as linear and nonlinear integer arithmetic.
Some tasks, notably those in the Arrays category, make use of arrays but
pointer aliasing is very limited. This class of tasks falls generally within
the capabilities of the solvers, albeit some are currently out of reach, e.g.
complex properties over arrays that require quantified invariants, or when
function summaries would need to be recursive.

We compare Z3 4.8.9 [37] and Eldarica 2.0.4 [33] as backends, the top two
performers in the CHC competition 2020 [51]. The hardware configuration is the
same as that of SV-COMP: Intel Xeon E3-1230 with 3.40 GHz and 8 cores, limited
to 15 min and 15 GB memory per individual task. The experiments have been
executed on Ubuntu 20.04 with Java 11 (for Korn and Eldarica), using benchexec
[4] for accurate resource management and measurement.

We evaluate three configurations of Korn:

  1. 1.

_Invariants only_ , with a translation using state predicates to represent
joint-points and invariants, using the conditions of Def. 3.

  2. 2.

_Summaries with safe invariants_ , using transition predicates to represent,
joint points and loop summaries, but with state predicates for invariants,
using the conditions of Def. 4.

  3. 3.

_A combination of the two_ , where we include the invariants as assumptions in
the constraints of summaries, such that the solver can choose either approach
to represent the correctness proof. This approach includes invariants as
additional assumptions in the conditions for the summaries, such that they are
available when a) propagating the summary backwards, and b) when proving the
postcondition of the loop. As such, the solver is in principle able to
instantiate a canonical summary like the one in Prop. 2. Join points and
similar are encoded using relations again such that summaries make sense.

For reference, we include official results777https://zenodo.org/record/3630205
from SV-COMP 2020 for CPA-seq [16] (“CPA $\checkmark$”), Ultimate Automizer
[28] (“UA”), and VeriAbs [1] (which can detect loop parallelism), but filtered
to the same set of 459 tasks (cf. “#”).

#### Results

Numeric results are shown in Table 1. Both solvers have trouble with the Array
category, which is difficult and subject to active research [17, 21]. VeriAbs
[1] performs well, because it can detect and exploit loop parallelism.
Category ControlFlow poses little trouble, most benchmarks are solved,
similarly for for Recursion. In category Loops, success is mixed, and here we
find the biggest differences between invariant-based and summary-based
approaches.

Eldarica can deal quite well with summaries, and instantiate these even if we
force the proof with these, missing out on 5 tasks wrt. invariants only. In
comparison, Z3 performs worse when summaries are present. For both backends,
the third configuration is in fact the most difficult, i.e., the choice
between encoding correctness into the invariant wrt. encoding it into the
summary harms performance, possibly because the problem is less constrained.

Table 1: Correct results, as found by the solvers, for the respective categories. # shows the number of tasks which are supported by Korn and thus evaluated vs. the total number of tasks in the category. Columns $I$ is configuration 1, column $R$ is configuration 2, and column $I,R$ is configuration 3. Tool |  | Korn | CPA$\checkmark$ | UA | VeriAbs
---|---|---|---|---|---
Backend |  | Eld. 2.0.4 [33] | Z3 4.8.9 [25] |  |  |
Category | #/total | $I$ | $R$ | $I,R$ | $I$ | $R$ | $I,R$ | (SV-COMP 2020)
Arrays | 129/436 | 2 | 2 | 2 | 7 | 2 | 2 | 3 | 3 | 122
ControlFlow | 39/ 95 | 36 | 36 | 36 | 31 | 33 | 33 | 37 | 37 | 31
Loops | 196/289 | 117 | 112 | 109 | 105 | 75 | 71 | 83 | 113 | 162
Recursion | 95/105 | 82 | 82 | 82 | 91 | 91 | 91 | 77 | 74 | 83
Sum | 459/925 | 237 | 229 | 232 | 234 | 201 | 197 | 200 | 227 | 398

Fig. 3 show a quantile plot of all correct results, which in addition to Table
1 reflects the solving times. The results for invariants are shown in red,
those with summaries only are shown in blue, and those with both in black. Z3
solves the majority of tasks well within a second, requiring more than ten
seconds only on the last few benchmarks. We also see that for the
configurations using summaries, if successful, Z3 still takes longer on
average. Eldarica, on the other hand, shows no such clear performance
difference between the configurations.

There are a few incorrect results per experimental setup (1 for Eldarica, and
2 resp. 3 for Z3, depending on the configuration). This is attributed to
limitations of the implementation in two cases (incorrect handling of numeric
operations with sizes of different types). For one task, recursive/Primes.c,
Z3 states that no solution exists, which is correct according insofar as no
_non-recursive_ solution exists (the tasks models arithmetic functions
recursively).

Figure 3: Quantile plot showing the relative performance of the three
approaches, in comparison to three top software verifiers on the same tasks.

#### Discussion

We can answer the research question outlined in the beginning positively:
Current Horn clause solvers are in fact able to instantiate summaries, and
their performance is roughly comparable to verification with plain invariants.
Nevertheless, the evaluation does have some limitations and specifics.

Many verification tasks require reasoning about integer arithmetic “only”,
which is a well-researched area. For instance, Eldarica employs abstract
numeric domains, which can represent many types of integer constraints very
efficiently. Moreover, such representations are complete wrt. certain classes
of constraints (e.g. nonlinear arithmetic). It is not too surprising that the
tasks that fall into this class are solved, regardless of the chosen Horn
clause encoding. Indeed, by manual inspection, there are quite a few such
tasks, and one might be inclined to state that the benchmark set may be too
easy.

On the other hand, consider the category Arrays, where we could hope that
summaries might be beneficial. From this evaluation we cannot draw a
conclusive answer, since the tasks are too hard for the Horn solvers
evaluated.

To gain further insight, the generated invariants would have to be compared to
the generated summaries, which we have not attempted to do systematically
here, as it would require significant additional effort. In the future, it
would be nice to mechanically compare the inferred predicates, e.g., by using
an SMT solver to check whether the instances fall into specific categories
(safe invariants, canonical summaries), and whether the safe invariants found
are actually weaker than their correct counterparts.

Possibly, the performance of the summary-based approach can be boosted by
specialized strategies, e.g., adapting that of VeriAbs, or by finding
generalizations as discussed in Sec. 2, using insights from [10] and from
rippling [11]. Similarly, inference of recursive solutions is an interesting
topic for future research, e.g., by syntax-guided techniques [3], or by the
approach in [48].

##  7 Related Work

We emphasize that the approach of using summaries, resp. loop specifications
in terms of pre-/postconditions is not new, see e.g. Hehner [26] for practical
examples. The work closest to the theory of Sec. 3 is by Hehner and Gravel
[27], which shows an analogue of Def. 4 as Rule F in [27, Sec 10]. Their
presentation is closely tied to reasoning about for-loops, where starting and
ending indices are known (as symbolic expressions). In contrast, we delimit
the loop in terms of precondition $P$ and postcondition $Q$, which lifts the
idea to all loops in general. Moreover, Rule F does not make explicit the
relational nature of summaries, whereas Rule G in [27] considers _two
arbitrary_ execution segments of the loop, instead of a single segment known
to end in a final state (cf. Fig. 2). Further work that is based on the same
idea essential is [9, 14]. A constructive translation like the one shown Sec.
4 is not provided there or elsewhere as far as we know.

We note that the approach presented here is not a backwards analysis where
transitions are reversed (e.g., [12]), as summaries propagate results
backwards.

Induction for the verification of loops (and also recursive procedures) occurs
in a variety of forms in practice, specifically when strong specifications are
desired and manual effort is acceptable. In the context of Separation Logic,
Tuerk [55] demonstrates verification rules with summaries, mechanized in the
HOL theorem prover, we refer back to Sec. 5 for a comparison. VeriFast offers
loop specifications in terms of pre-/postconditions, with first-class support
for applying the inductive hypothesis, which was used to solve a challenge
with linked trees in the VerifyThis competition 2012 (Jacobs et al. [36]).
Tools that embed program verification into a general purpose theorem prover
can make use of explicit induction, too, as shown e.g. with KIV (for the same
challenge, Ernst et al. [19]). The support for magic wands in Schwerhoff and
Summers [53] resembles the encoding of summaries as invariants via (2).
Alternatively, loops can be turned into recursive procedures to aid
verification [46].

A proof system based on coinduction (i.e. forward reasoning) that generalizes
loop verification to any recurring program locations is [15], a similar
approach to tackle interleavings in concurrency is [52]. Brotherston [10]
takes a similar route to construct cyclic proofs, implicitly making use of
induction. All three approaches have in common that the inductive property is
constructed on the fly instead of being expressed by a fixed predicate or
formula up-front.

Recent work on the verification of unstructured assembly programs [41] notes
that a negative loop test $\lnot t$ cannot be assumed by default in such a
setting, as it is the case with the conditions Def. 4. As discussed, our
approach can include this conclusion as part of the summary, in the absence of
early loop exits. An interesting verification challenge is Duff’s device, with
unstructured _entries_ into a loop [54].

Even though the benefits of loop specifications have been established, the
technique is less prominent in fully automatic verification. For instance, the
tools participating in SV-COMP [5] show a strong bias towards invariants. As
an example, the most successful configuration of CPAchecker [7], CPA-seq,
relies on k-Induction [18, 6], which exploits correctness constraints from
inside the loop body, but disregards the constraints after a particular loop
for its verification. Likewise, Property Directed Reachability [42] reasons
forward over loops, but it is more precise wrt. different stages of a
computation; Z3’s fixpoint engine is fundamentally based on this idea [32,
38].

Ultimate Automizer [29] abstracts traces in terms of automata, which may
contain loops. Whether there is a more fundamental connection between their
approach and loop summaries is not quite clear, and we leave this question for
future work. SeaHorn [24] is a verification platform for Horn clause based
verification of C programs, using the invariant approach. We are not aware of
an attempt to leverage Horn solvers for the inference of summaries.

In Spark/GNATprove, loop invariants can be specified to hold anywhere in the
loop body [30], and there is an equivalent to old, referring to the state of
the loop entry. The approach is demonstrated with a verification of the
prefixsum algorithm, a tricky challenge from VerifyThis 2012 [35]. The
approach bears resemblance to k-Induction [18], because correctness conditions
are reflected inside the loop, not in the code that follows as with summaries.

While orthogonal, progress in solving Horn clauses [21, 56, 33, 13, 23, 22,
17] among others, see also [51], will improve performance of this work in the
future.

##  8 Conclusion and Outlook

This paper presents a concise and accessible formulation of loop summaries,
which generalizes Hoare’s [31] proof approach for loops using invariants, and
Hehner’s refinement-based approach [27]. The presentation sheds light into
fundamental properties of the approach, and we prove several novel results,
that are not only theoretical but offer immediate guidelines for tool
construction: We characterize, which part of the proof may be expressed using
summaries, and which part must be covered by invariants (Thm. 3.4). Moreover,
we demonstrate that the approaches can represent each other, giving
constructive translations between them (Props. 1 and 2).

The evaluation shows that state-of-the-art solvers can instantiate summaries
almost as well as they can find invariants, for a substantial set of standard
benchmarks. There are several clear paths forward, outlined in Sec. 6, to
further leverage the potential of summaries for proof automation.

Summaries are thus a fundamental and principled technique, complementary to
invariants in theory and in practice.

#### Acknowledgement.

Thanks to Toby Murray for valuable feedback. The presentation in Sec. 5 is
part of Gregor Alexandru’s bachelor thesis [2]. The treatment of break and
goto in with summaries has been explored by Johannes Blau.

## References

  * Afzal et al. [2020] Afzal, M., Chakraborty, S., Chauhan, A., Chimdyalwar, B., Darke, P., Gupta, A., Kumar, S., Babu, C., Unadkat, D., Venkatesh, R.: Veriabs: Verification by abstraction and test generation (competition contribution).  In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 383–387. Springer (2020)
  * Alexandru [2019] Alexandru, G.: Specifying loops with contracts (2019), Bachelor’s Thesis, LMU Munich
  * Alur et al. [2013] Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis.  IEEE (2013)
  * Beyer [2016] Beyer, D.: Reliable and reproducible competition results with benchexec and witnesses (report on sv-comp 2016).  In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 887–904. Springer (2016)
  * Beyer [2020] Beyer, D.: Advances in automatic software verification: Sv-comp 2020.  In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 347–367. Springer (2020)
  * Beyer et al. [2018] Beyer, D., Dangl, M., Wendler, P.: A unifying view on smt-based software verification.  Journal of Automated Reasoning 60(3), 299–335 (2018)
  * Beyer and Keremoglu [2011] Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification.  In: Computer Aided Verification. pp. 184–190. Springer (2011)
  * Bjørner et al. [2015] Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification.  In: Fields of Logic and Computation II, pp. 24–51. Springer (2015)
  * Bohórquez [2010] Bohórquez, J.: An elementary and unified approach to program correctness.  Formal aspects of computing 22, 611–627 (2010)
  * Brotherston [2005] Brotherston, J.: Cyclic proofs for first-order logic with inductive definitions.  In: Automated Reasoning with Analytic Tableaux and Related Methods. pp. 78–92. Springer (2005)
  * Bundy et al. [1993] Bundy, A., Stevens, A., Van Harmelen, F., Ireland, A., Smaill, A.: Rippling: A heuristic for guiding inductive proofs (1993)
  * Cabodi et al. [1994] Cabodi, G., Camurati, P., Quer, S.: Efficient state space pruning in symbolic backward traversal.  In: VLSI in Computers and Processors. pp. 230–235. IEEE (1994)
  * Champion et al. [2018] Champion, A., Kobayashi, N., Sato, R.: Hoice: An ice-based non-linear horn clause solver.  In: Asian Symposium on Programming Languages and Systems. pp. 146–156. Springer (2018)
  * Charguéraud [2010] Charguéraud, A.: Characteristic formulae for mechanized program verification.  Ph.D. thesis, PhD thesis, Université Paris-Diderot (2010)
  * Chen et al. [2020] Chen, X., Trinh, M.T., Rodrigues, N., Peña, L., Rosu, G.: Towards a unified proof framework for automated fixpoint reasoning using matching logic.  Tech. rep. (2020)
  * Dangl et al. [2015] Dangl, M., Löwe, S., Wendler, P.: Cpachecker with support for recursive programs and floating-point arithmetic.  In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 423–425. Springer (2015)
  * De Angelis et al. [2014] De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying array programs by transforming verification conditions.  In: Verification, Model Checking, and Abstract Interpretation. pp. 182–202. Springer (2014)
  * Donaldson et al. [2011] Donaldson, A.F., Haller, L., Kroening, D., Rümmer, P.: Software verification using k-induction.  In: International Static Analysis Symposium. pp. 351–368. Springer (2011)
  * Ernst et al. [2015] Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV—Overview and VerifyThis competition.  Software Tools for Technology Transfer (STTT) 17(6), 677–694 (2015)
  * Ernst [2020] Ernst, G.: A complete approach to loop verification with invariants and summaries (2020), https://arxiv.org/abs/2010.05812, extended version
  * Fedyukovich et al. [2019] Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis.  In: Computer Aided Verification. pp. 259–277. Springer (2019)
  * Grebenshchikov et al. [2012] Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules.  ACM SIGPLAN Notices 47(6), 405–416 (2012)
  * Gurfinkel and Bjørner [2019] Gurfinkel, A., Bjørner, N.: The science, art, and magic of constrained horn clauses.  In: 2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). pp. 6–10. IEEE (2019)
  * Gurfinkel et al. [2015] Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework.  In: Computer Aided Verification. pp. 343–361. Springer (2015)
  * Gurfinkel et al. [2016] Gurfinkel, A., Shoham, S., Meshman, Y.: Smt-based verification of parameterized systems.  In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 338–348 (2016)
  * Hehner [2005] Hehner, E.C.: Specified blocks.  In: Working Conference on Verified Software: Theories, Tools, and Experiments. pp. 384–391. Springer (2005)
  * Hehner and Gravel [1999] Hehner, E.C., Gravel, A.M.: Refinement semantics and loop rules.  In: International Symposium on Formal Methods. pp. 1497–1510. Springer (1999)
  * Heizmann et al. [2018] Heizmann, M., Chen, Y.F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., et al.: Ultimate automizer and the search for perfect interpolants.  In: Tools and Algorithms for the Construction and Analysis of Systems. pp. 447–451. Springer (2018)
  * Heizmann et al. [2009] Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction.  In: International Static Analysis Symposium. pp. 69–85. Springer (2009)
  * Hoang et al. [2015] Hoang, D., Moy, Y., Wallenburg, A., Chapman, R.: Spark 2014 and gnatprove.  International Journal on Software Tools for Technology Transfer 17(6), 695–707 (2015)
  * Hoare [1969] Hoare, C.A.R.: An axiomatic basis for computer programming.  Communications of the ACM 12(10), 576–580 (1969)
  * Hoder et al. [2011] Hoder, K., Bjørner, N., De Moura, L.: $\mu$z–an efficient engine for fixed points with constraints.  In: Computer Aided Verification. pp. 457–462. Springer (2011)
  * Hojjat and Rümmer [2018] Hojjat, H., Rümmer, P.: The eldarica horn solver.  In: 2018 Formal Methods in Computer Aided Design (FMCAD). pp. 1–7. IEEE (2018)
  * Huisman and Jacobs [2000] Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination.  In: Fundamental Approaches to Software Engineering. pp. 284–303. Springer (2000)
  * Huisman et al. [2013] Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2012: Organizers report.  Tech. rep., KIT, Fakultät für Informatik (2013)
  * Jacobs et al. [2015] Jacobs, B., Smans, J., Piessens, F.: Solving the VerifyThis 2012 challenges with VeriFast.  International Journal on Software Tools for Technology Transfer 17(6), 659–676 (2015)
  * Komuravelli et al. [2016] Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs.  Formal Methods in System Design 48(3), 175–205 (2016)
  * Komuravelli et al. [2013] Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in smt-based unbounded software model checking.  In: Computer Aided Verification. pp. 846–862. Springer (2013)
  * Leino [2008] Leino, K.R.M.: This is Boogie 2 (2008)
  * Leino [2010] Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness.  In: Logic for Programming Artificial Intelligence and Reasoning. pp. 348–370. Springer (2010)
  * Lundberg et al. [2020] Lundberg, D., Guanciale, R., Lindner, A., Dam, M.: Hoare-style logic for unstructured programs.  In: Software Engineering and Formal Methods. pp. 193–213. Springer (2020)
  * McMillan [2003] McMillan, K.L.: Interpolation and sat-based model checking.  In: Computer Aided Verification. pp. 1–13. Springer (2003)
  * Morgan [1988] Morgan, C.: The specification statement.  ACM Transactions on Programming Languages and Systems (TOPLAS) 10(3), 403–419 (1988)
  * Mraihi et al. [2013] Mraihi, O., Louhichi, A., Jilani, L.L., Desharnais, J., Mili, A.: Invariant assertions, invariant relations, and invariant functions.  Science of Computer Programming 78(9), 1212–1239 (2013)
  * Müller et al. [2016] Müller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution.  In: Computer Aided Verification. pp. 405–425. Springer (2016)
  * Myreen and Gordon [2009] Myreen, M.O., Gordon, M.J.: Transforming programs into recursive functions.  Electronic Notes in Theoretical Comp. Science 240, 185–200 (2009)
  * Nipkow et al. [2002] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: a proof assistant for higher-order logic, vol. 2283.  Springer Science & Business Media (2002)
  * Reynolds et al. [2016] Reynolds, A., Blanchette, J.C., Cruanes, S., Tinelli, C.: Model finding for recursive functions in smt.  In: International Joint Conference on Automated Reasoning. pp. 133–151. Springer (2016)
  * Reynolds [2002] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures.  In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74. IEEE (2002)
  * Roşu and Lucanu [2009] Roşu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation.  In: Algebra and Coalgebra in Computer Science. pp. 127–144. Springer (2009)
  * Rümmer [2020] Rümmer, P.: Competition report: Chc-comp-20.  arXiv preprint arXiv:2008.02939 (2020)
  * Schellhorn et al. [2014] Schellhorn, G., Tofan, B., Ernst, G., Pfähler, J., Reif, W.: Rgitl: A temporal logic framework for compositional reasoning about interleaved programs.  Annals of Mathematics and Artificial Intelligence 71(1-3), 131–174 (2014)
  * Schwerhoff and Summers [2015] Schwerhoff, M., Summers, A.J.: Lightweight suppoert for magic wands in an automatic verifier.  In: 29th European Conference on Object-Oriented Programming (ECOOP 2015). vol. 37, pp. 614–638. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2015)
  * Tews [2004] Tews, H.: Verifying duff’s device (2004)
  * Tuerk [2010] Tuerk, T.: Local reasoning about while-loops.  VSTTE 2010, 29 (2010)
  * Unno et al. [2017] Unno, H., Torii, S., Sakamoto, H.: Automating induction for solving horn clauses.  In: Computer Aided Verification. pp. 571–591. Springer (2017)