# Finding Inductive Loop Invariants using Large Language Models

Adharsh Kamath  Microsoft ResearchIndia<EMAIL_ADDRESS>,  Aditya
Senthilnathan  CornellUSA<EMAIL_ADDRESS>,  Saikat Chakraborty  Microsoft
ResearchUSA<EMAIL_ADDRESS>,  Pantazis Deligiannis  Microsoft
ResearchUSA<EMAIL_ADDRESS>,  Shuvendu K. Lahiri  Microsoft
ResearchUSA<EMAIL_ADDRESS>,  Akash Lal  Microsoft ResearchIndia
<EMAIL_ADDRESS>,  Aseem Rastogi  Microsoft ResearchIndia
<EMAIL_ADDRESS>,  Subhajit Roy  IIT KanpurIndia<EMAIL_ADDRESS>and
Rahul Sharma  Microsoft ResearchIndia<EMAIL_ADDRESS>
###### Abstract.

Loop invariants are fundamental to reasoning about programs with loops. They
establish properties about a given loop’s behavior. When they additionally are
inductive, they become useful for the task of formal verification that seeks
to establish strong mathematical guarantees about program’s runtime behavior.
The inductiveness ensures that the invariants can be checked locally without
consulting the entire program, thus are indispensable artifacts in a formal
proof of correctness.

Finding inductive loop invariants is an undecidable problem, and despite a
long history of research towards practical solutions, it remains far from a
solved problem. This paper investigates the capabilities of the Large Language
Models (LLMs) in offering a new solution towards this old, yet important
problem.

To that end, we first curate a dataset of verification problems on programs
with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive
loop invariants, that are checked for correctness using sound symbolic tools.
Finally, we explore the effectiveness of using an efficient combination of a
symbolic tool and an LLM on our dataset, and compare it against a purely
symbolic baseline. Our results demonstrate that LLMs can help improve the
state-of-the-art in automated program verification.

##  1\. Introduction

Automatically synthesizing loop invariants is one of the classical problems in
software verification. A variety of techniques have been developed to address
it over multiple decades, each with their own strengths and weaknesses. With
the advent of Large Language Models (LLMs), we study how well LLMs perform on
this problem. To that end, we collect a dataset of programs in the C language
and build a toolchain that can evaluate the success rate of a given LLM on the
dataset.

Loop invariant is a logical proposition that is valid at the head of a given
loop, irrespective of how many times the loop has already, or will execute.
Inductiveness of loop invariants further requires that one can prove its
correctness just by looking at the loop body, not the rest of the program;
further the invariant is strong enough to establish the property of interest.
More formally, the problem of inductive loop invariant inference can be
described as follows. Consider a Hoare triple (hoare1969axiomatic, ) over a
loop $\\{P\\}\mathit{while}\ B\ \mathit{do}\ S\\{Q\\}$, which states that $P$
is a precondition that holds before the loop, and $Q$ is the postcondition
that holds after the loop (on terminating executions). Proving this Hoare
triple is valid requires finding an inductive loop invariant, i.e., an
expression $\mathcal{I}$ such that the following three conditions hold. First,
the loop invariant must be implied by the precondition
($P\Rightarrow\mathcal{I}$). Second, given that $\mathcal{I}$ holds at the
head of the loop, and the loop executes for one arbitrary iteration, then
$\mathcal{I}$ must continue to hold at the end of the loop iteration
($\\{\mathcal{I}\wedge B\\}S\\{\mathcal{I}\\}$). And finally, when the loop
exits, then the loop invariant must imply $Q$ ($\mathcal{I}\wedge\neg
B\Rightarrow Q$). For the sake of simplicity, we assume that the qualifier
“inductive” is assumed and refer to such expressions $\mathcal{I}$ as loop
invariants.

#### Example.

Consider the example of a Hoare-triple for a loop in a C-like language where
the variables are unbounded integers that do not overflow:

$\\{n\geq 0\wedge x==n\wedge y==0\\}\mathit{while}\ (x>0)\ \mathit{do}\
x--;y++;\\{y==n\\}$

The goal is to prove the postcondition $y==n$ on exit from the loop, when the
loop is executed starting with a non-negative value $n$ in variable $x$. The
invariant $\mathcal{I}\doteq\left(x+y==n\wedge x\geq 0\right)$ is inductive
because the following conditions hold:

  1. (1)

the precondition implies the invariant, namely

$\left(n\geq 0\wedge x==n\wedge y==0\right)\implies\left(x+y==n\wedge x\geq
0\right)$

  2. (2)

the invariant is preserved by the loop body, namely

$\\{\left(x+y==n\wedge x\geq
0\right)\wedge(x>0)\\}x--;y++\\{\left(x+y==n\wedge x\geq 0\right)\\}$

  3. (3)

the invariant implies the postcondition on exit, namely

$\left(\left(x+y==n\wedge x\geq 0\right)\wedge\neg(x>0)\right)\implies y==n$

Further, the three checks above can be efficiently expressed in a decidable
logic and verified using Satisfiability-Modulo-Theories (SMT) (BarFT-SMTLIB, )
solvers.

In contrast, the problem of finding loop invariants is undecidable in general.
Earlier works have resorted to several heuristics. Symbolic techniques include
counter-example guided abstraction refinement
(DBLP:journals/jacm/ClarkeGJLV03, ; ball-pldi01, ), Craig interpolation
(mcmillan-cav03, ), abstract interpretation with various abstract domains
(cousot-77, ; blanchet-pldi03, ), syntax-guided synthesis (alur2013syntax, ),
among others. Machine-learning-based techniques have been applied as well,
including classical learning over data generated from program executions
(loopinvgen_padhi, ; DBLP:conf/sas/BrockschmidtCKK17, ), active learning over
decision trees (garg-popl16, ), reinforcement learning over graph neural
networks (si2018learning, ), and the use of continuous logic networks
(yao2020learning, ; ryancln2inv, ). Tools based on these techniques compete in
the invariant inference tracks of competitions like the software verification
competition (SV-COMP) (svcomp, ) and the synthesis competition (SyGuS) (sygus,
).

LLMs are now being routinely used to assist software developers (copilot, ),
which leads to the natural question of whether they can assist in annotating
loop invariants as well. We use LLMs to generate candidate loop invariants
that can then be checked by a symbolic verification tool like FRAMA-C
(DBLP:journals/fac/KirchnerKPSY15, ) or Boogie (barnett05, ). These verifiers
take a program annotated with loop invariants as input and check the validity
of the Hoare triple. If the LLM generates a wrong candidate then the candidate
is rejected. But if the checker passes then it has successfully demonstrated
the validity of the Hoare triple.

#### Contributions

We have curated a dataset of loop invariant inference problems from several
prior works on invariant inference, with the goal of evaluating LLMs for the
task of loop invariant generation. We have also built a toolchain that
evaluates a given LLM on this dataset, both for invariant generation as well
as repair. We evaluate multiple models (GPT-4
(DBLP:journals/corr/abs-2303-08774, ), GPT-3.5 (gpt35, ), and Code Llama
(DBLP:journals/corr/abs-2307-09288, )) and compare their performance against a
state-of-the-art symbolic baseline. We further contribute a novel combination
of LLMs with symbolic techniques that help tolerate inaccuracies in the
model’s output, only relying on the model to produce ingredients of the loop
invariant rather than the whole invariant. This combination only requires a
linear number of calls to the underlying symbolic solver (linear in the number
of LLM generations).

In the rest of the paper, we describe this dataset (Section 2), technical
details (Section 3), evaluation (Section 4), and related work (Section 5).

##  2\. Dataset

We collect benchmarks from the sources listed in LoopInvGen (loopinvgen_padhi,
). These include all the benchmarks from prior works - Code2Inv (code2Inv, ),
Accelerating Invariant Generation (accelerating_invariant_gen, ), and
LinearArbitrary-SeaHorn (linear_arbitrary_seahorn, ). We also collect
benchmarks from SV-COMP (SVCOMP23, ), specifically, its sub-directories
starting with the prefix ”loop”. In total, this combined set contains 1166
benchmarks. Each benchmark is a program in the C language, where the property
to be verified is present implictly in the form of assertions in the program
itself. Successful verification of a program guarantees that every assertion
in the program is valid in all executions of the program.

We restrict to integer programs by filtering out benchmarks that have arrays
or pointers. This keeps the focus on basic mathematical reasoning, without
bringing in concerns of modeling heap semantics in C. We also filter out
programs with ambiguous semantics.111Some programs had the pattern
if(assert(expression)) with no clear indication of what assert is supposed to
return. We also removed programs that are greater than 500 lines of code to
account for current prompt size limitations in LLMs. This leaves us with 1005
benchmarks. We categorize these benchmarks based on the number of loops and
methods, as shown in Table 1.

| Number of | Methods
---|---|---
| benchmarks | Exactly one | More than one
| None | 58 | 122
Loops | Exactly one | 555 | 30
| More than one | 214 | 26
Table 1. Benchmark features

Of these categories, we focus on the 555 benchmarks with exactly one loop and
one method. Out of these 555 benchmarks, 469 are positive instances, i.e.,
there exists an invariant that is sufficient to verify all the assertions in
the benchmark and 86 benchmarks are negative instances, i.e., there exists a
counterexample that violates some assertion. The ground truth for each
benchmark was obtained using a combination of the original benchmark source,
Ultimate Automizer (automizer, ) and manual inspection.

We make modifications to the 469 benchmarks to remove comments, modify calls
to verifier-specific assert functions to ACSL assert annotations, etc., and
create the final dataset used in the experiments. (ACSL (e_acsl_user_manual, )
is the syntax that Frama-C uses for writing logical specifications.) These
modifications do not alter the semantics of the programs in any way with
respect to the property being verified. A detailed list of these modifications
can be found in Appendix A.2.

##  3\. Technical details

Our toolchain has two main components, a large language model,
$\mathcalorig{L}$, and an oracle $\mathcalorig{O}$. The input to
$\mathcalorig{L}$ is text that consists of two parts: (1) Prompt template
$\mathcalorig{M}$ that contains instructions relevant to finding loop
invariants, common for all programs and (2) the target program
$\mathcalorig{P}$, with a property to be verified in the form of assertions
present in the program text. The output of $\mathcalorig{L}$ is a set of
candidate loop invariants $\mathcalorig{I}$ in the format specified in
$\mathcalorig{M}$. We may query $\mathcalorig{L}$ to generate multiple
completions with a non-zero sampling temperature, to generate different sets
of candidate invariants.

The oracle $\mathcalorig{O}$ checks if a given set of candidate invariants are
inductive and sufficient for verifying the program. The input to
$\mathcalorig{O}$ is $\mathcalorig{P}$ annotated with a given set of candidate
invariants $\mathcalorig{I}$; we refer to this annotated program as
$\mathcalorig{A}$($\mathcalorig{P}$, $\mathcalorig{I}$). The actual
implementation of $\mathcalorig{A}$ depends on the particular formatting
requirements of the orcale $\mathcalorig{O}$.

The output of $\mathcalorig{O}$ is a tuple consisting of the following values:

  1. (1)

A Boolean value $S$. If $S$ is true, then all the supplied candidate
invariants were correct invariants of the program and were sufficient to prove
correctness of the assertions as well.

  2. (2)

A string value $SyntaxError$ indicating if the oracle encountered a syntax
error while parsing some candidate invariant expression. This string is
necessarily empty if $S$ was true. When non-empty, $SyntaxError$ indicates the
location (i.e., the candidate expression) that caused the syntax error to
happen.

  3. (3)

A set ${I}_{L}$ that is empty when $S$ is true or if there was a syntax error.
Otherwise, it is a subset of the supplied candidate invariants. The
expectation on the oracle is that whenever it fails to prove inductiveness of
a set of candidate invariants, it must indicate the reason by putting blame on
at least one of the candidates. This property will be made more precise later
in this section.

We describe our toolchain in the next three subsections, outlining the overall
technique (Section 3.1), and two components Houdini (Section 3.2) and Repair
(Section 3.3).

###  3.1. Loopy

Our technique—called Loopy—is detailed in Algorithm 1. The loop on line 6
iterates as many times as the user-provided bound $\mathcalorig{N}_{s}$ on the
number of completions. For each completion, it checks if the LLM-returned set
of candidate invariants are correct. If so, the entire procedure completes.

Even when none of the completions individually were a correct set of
invariants, it could happen that the necessary correct invariants were spread
across the multiple sets. To deal with such cases, Loopy computes
$\mathcalorig{I}_{u}$ as the union of all the candidate invariant sets that
were generated across multiple completions. Next, it checks if there exists a
subset $\mathcalorig{I}_{s}\subseteq\mathcalorig{I}_{u}$ that is inductive and
sufficient for verifying the program. While there may be an exponential number
of possible subsets of $\mathcalorig{I}_{u}$, it turns out that one can do
this check with only a linear number of calls to the oracle (linear in the
size of $\mathcalorig{I}_{u}$), using the Houdini algorithm (houdini, ).

If Houdini is not successful, Loopy calls a procedure to repair the existing
set of all LLM-generated invariants $\mathcalorig{I}_{u}$ in line 20.

Algorithm 1 Loopy procedure

1:Program $\mathcalorig{P}$, Prompt $\mathcalorig{M}$, number of times to
sample invariants, $\mathcalorig{N}_{s}$, and number of repair retries,
$\mathcalorig{N}_{r}$

2:True iff all the assertions in $\mathcalorig{P}$ are verified, False
otherwise

3:Set of inductive invariants when the program was verified

4:procedure
Loopy($\mathcalorig{P},\mathcalorig{M},\mathcalorig{N}_{s},\mathcalorig{N}_{r}$)

5: $\mathcalorig{I}_{u}\leftarrow\\{\\}$

6: while $\mathcalorig{N}_{s}>0$ do

7: $\mathcalorig{I}\leftarrow\mathcalorig{L}(\mathcalorig{M},\mathcalorig{P})$
$\triangleright$ Prompt the LLM

8:
$S,\\_,\\_\leftarrow\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$
$\triangleright$ Annotate the program and check

9: if $S$ = True then

10: return True, $\mathcalorig{I}$

11: else

12: $\mathcalorig{N}_{s}\leftarrow\mathcalorig{N}_{s}-1$

13: $\mathcalorig{I}_{u}\leftarrow\mathcalorig{I}_{u}\cup\mathcalorig{I}$

14: end if

15: end while

16:
$S,\mathcalorig{I}\leftarrow\textsc{Houdini}(\mathcalorig{P},\mathcalorig{I}_{u})$
$\triangleright$ Algorithm 2

17: if $S$ = True then

18: return True, $\mathcalorig{I}$

19: else

20:
$S,\mathcalorig{I}\leftarrow\textsc{Repair}(\mathcalorig{P},\mathcalorig{I}_{u},\mathcalorig{N}_{r})$
$\triangleright$ Algorithm 3

21: return $S,\mathcalorig{I}$

22: end if

23:end procedure

###  3.2. Houdini

We describe an adaptation of Houdini to our setting in Algorithm 2. This
procedure takes as input the program $\mathcalorig{P}$ and a set of invariants
$\mathcalorig{I}$ and returns $\mathit{True}$ if there exists a subset of
$\mathcalorig{I}$ that is inductive and sufficient for verification, and
$\mathit{False}$ otherwise.

Houdini works by repeatedly querying the oracle with its current set of
candidate invariants $\mathcalorig{I}$. In each iteration, it either finds
that $\mathcalorig{I}$ is sufficient, in which case it is done and returns
True (line 7). Otherwise, it removes one or more candidates from the set
$\mathcalorig{I}$ and repeats the process. Pruning happens in one of two ways.
If an expression causes a syntax error, then it is pruned away (line 10). If
there are no syntax errors, then the expressions in $I_{L}$ are pruned away
(line 15). If $I_{L}$ was empty, then the procedure returns False; this
indicates the case when the current set $\mathcalorig{I}$ is a valid inductive
invariant, but still not sufficient (i.e., strong enough) to prove the program
correct.

A candidate might not be inductive for one of two reasons. It might not hold
on entry to the loop (i.e., not implied by the precondition), or that it may
not be preserved by the loop body. The complication is that preservation of
one candidate might rely on other candidates. Thus, we require that for each
candidate $i$ that is included in $I_{L}$ by the oracle, either $i$ did not
hold at entry to the loop, or that $i$ was not preserved even when assuming
all candidate invariants (even failed ones) to hold at the beginning of the
loop iteration. There must be at least one such candidate if the candidate set
is not collectively inductive. In other words, there is no support for
candidates in $I_{L}$ to be inductive invariants, whereas the rest of the
candidates might still be proved inductive. Checkers such as Frama-C
(DBLP:journals/fac/KirchnerKPSY15, ) and Boogie (barnett05, ) are able to
provide such information. However, we do note that this property is only
required for optimality of Houdini. Irrespective of how $I_{L}$ is populated,
the guarantee that Algorithm 2 returns an inductive set of invariants when it
returns true is a valid guarantee. It is just that Algorithm 2 might miss
finding a valid subset among the candidates even when one exists.

Furthermore, note that Houdini makes a linear number of calls to the Oracle –
at most as many calls as the size of the input candidate invariant set.

Algorithm 2 Houdini procedure

1:Program $\mathcalorig{P}$ and a set of invariants $\mathcalorig{I}$

2:(True, $\mathcalorig{I}_{0}$) if there exists
$\mathcalorig{I}_{0}\subseteq\mathcalorig{I}$ such that
$\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}_{0}))$ is
True. (False,$\\{\\}$) otherwise

3:procedure Houdini($\mathcalorig{P}$, $\mathcalorig{I}$)

4: while $\lvert\mathcalorig{I}\lvert\>>0$ do

5:
$S,I_{L},SyntaxError\leftarrow\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$)
$\triangleright$ Annotate the program and check

6: if $S=True$ then

7: return (True, $\mathcalorig{I}$)

8: end if

9: if $SyntaxError$ = “error while parsing invariant $i$” then

10: $\mathcalorig{I}\leftarrow\mathcalorig{I}-\\{i\\}$

11: else

12: if $I_{L}==\\{\\}$ then

13: break

14: else

15: $\mathcalorig{I}\leftarrow\mathcalorig{I}-I_{L}$

16: end if

17: end if

18: end while

19: return (False, $\\{\\}$)

20:end procedure

###  3.3. Repair

The Repair procedure takes a set of invariants $\mathcalorig{I}$ and attempts
to repeatedly generate a new set of invariants $\mathcalorig{I}^{\prime}$ that
are ”close” to $\mathcalorig{I}$ but contains an inductive subset. It either
returns (True, $\mathcalorig{I}^{\prime}$) where $\mathcalorig{I}^{\prime}$ is
inductive, or returns (False,$\\{\\}$).

The procedure, shown as Algorithm 3, repeatedly calls the oracle
$\mathcalorig{O}$ on a set of invariants $\mathcalorig{I}$ (lines 4 and 8) and
then queries the LLM $\mathcalorig{L}$ to repair the set of invariants using a
repair prompt $\mathcalorig{M}_{r}$ over the error information present in
$I_{L}$ and $SyntaxError$ (line 7). Details of the prompt are present in
Appendix A.1. The new set of invariants is queried for inductiveness (line 8)
or passed to Houdini procedure to find an inductive subset (line 12). The
process is repeated for $\mathcalorig{N}_{r}$ times, after which the procedure
returns (False,$\\{\\}$) to indicate failure.

Algorithm 3 Repair procedure

1:Program $\mathcalorig{P}$, a set of invariants $\mathcalorig{I}$, and number
of repair retries $\mathcalorig{N}_{r}$

2:(True, $\mathcalorig{I}^{\prime}$) if
$\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}^{\prime}))$
is True. (False,$\\{\\}$) otherwise

3:procedure repair($\mathcalorig{P},\mathcalorig{I},\mathcalorig{N}_{r}$)

4:
$S,I_{L},SyntaxError\leftarrow\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$

5: $n\leftarrow 0$

6: while $n<\mathcalorig{N}_{r}$ do

7:
$\mathcalorig{I}\leftarrow\mathcalorig{L}(\mathcalorig{M}_{r}(I_{L},SyntaxError),\>\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$
$\triangleright$ Instruct the LLM to repair

8:
$S,I_{L},SyntaxError\leftarrow\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$
$\triangleright$ Use the new invariants to verify

9: if $S=True$ then

10: return $(True,\mathcalorig{I})$

11: else

12:
$S,\mathcalorig{I}^{\prime}\leftarrow\textsc{Houdini}(\mathcalorig{P},\mathcalorig{I})$
$\triangleright$ Algorithm 2

13: if $S=True$ then

14: return $(True,\mathcalorig{I}^{\prime})$

15: else

16: $n\leftarrow n+1$

17: end if

18: end if

19: end while

20: return $(False,\\{\\})$

21:end procedure

##  4\. Evaluation

We design our experiments with the goal of answering the following research
questions. We call a candidate set of invariants $\mathcalorig{I}$ as correct
for a program $\mathcalorig{P}$ when
$\mathcalorig{O}(\mathcalorig{A}(\mathcalorig{P},\mathcalorig{I}))$ returns
true.

  1. RQ1

How often can LLMs generate a correct set of loop invariants for a C program?

  2. RQ2

How often can LLMs generate elements of a correct set of loop invariants
needed to verify a C program?

  3. RQ3

How do different foundational models compare in their ability to find
inductive invariants?

  4. RQ4

How often can LLMs fix incorrect invariants using error messages from the
oracle?

  5. RQ5

What are the program features where LLMs fail to generate correct invariants?

  6. RQ6

How does the performance of Loopy compare with state-of-the-art symbolic
verifiers?

#### Experimental setup

To answer these RQs, we instantiate the previously described toolchain with
Frama-C as the oracle $\mathcalorig{O}$, and GPT-4, GPT-3.5-Turbo, and
CodeLlama-34b-Instruct as the Large language model $\mathcalorig{L}$. Frama-C
was configured to use only the WP plugin for verification, which is suited to
check ACSL annotations in C programs. Note that Frama-C does not attempt
constructing inductive invariant on its own, rather it is focused on verifying
the correctness of any candidate invariants as well as assertions in the
program that it is given as input. Additionally, the WP plugin was configured
to use Z3 (z3, ), Alt-Ergo (alt-ergo, ), and CVC4 (cvc4, ) as the external
provers, with a timeout of 3 seconds.

We use a symbolic tool Ultimate Automizer (automizer, ) to establish a
symbolic baseline performance. Ultimate’s goal is to either establish
invariants that prove program correctness, or return a counterexample. It
provides a strong baseline comparison because it has been competing in the
software verification competition SV-COMP (svcomp, ), which largely contains a
superset of our dataset, for a number of years and winning in several
categories. Ultimate was configured with a core-toolchain timeout of 300
seconds. Commonly used tool configurations are included with releases of
Ultimate Automizer. Of these configurations, we use AutomizerReach.xml as the
toolchain file, and svcomp-Reach-64bit-Automizer_Default.epf as the settings
file.

LLM hyper-parameters that we used are given in Appendix A.1.

Figure 1. Success rate of Loopy with GPT-4 as the number of completions is
varied. Dashed lines depict the performance of Loopy without Houdini and
without Repair, for different prompts. Solid lines depict the performance of
Loopy with Houdini, but without Repair.

###  4.1. [RQ1] Using LLMs to generate loop invariants

To answer RQ1, we measure the number of benchmarks for which the Loopy
procedure (Algorithm 1) successfully verifies the benchmark program without
calling either Houdini or the Repair procedures.

We experimented with two different prompts. Prompt $\mathcalorig{M}_{1}$
includes the input program and simply asks for loop invariants. Prompt
$\mathcalorig{M}_{2}$ additionally includes instructions that detail the
concept of a loop invariant and additionally include certain hints or “nudges”
that offer guidelines on patterns that a loop invariant might contain. These
nudges are generic and not tailored to specific program instances. We include
both these prompts in Appendix A.1.

Results are reported in Figure 1; consider only the dashed lines for now. It
shows success rate of Loopy (number of benchmarks verified) as the number of
completions is varied. We account for the non-deterministic nature of LLMs in
the standard way followed when computing the “pass@k” metric as described in
Chen et al. (codex, ): we first generate the maximum number of completions
($15$) and compute its success rate. Then, the success rate for $k$
completions is obtained as the expectation over a random sample of size $k$
out of the $15$ completions.

The figure shows that multiple completions help, although there are
diminishing returns after around $8$ completions. Adding instructions to the
prompt helps, with $\mathcalorig{M}_{2}$ performing significantly better than
$\mathcalorig{M}_{1}$. Prompt $\mathcalorig{M}_{2}$ helps solve $23\%$ more
instances than prompt $\mathcalorig{M}_{1}$ (293 benchmarks for
$\mathcalorig{M}_{2}$, compared to 237 benchmarks for $\mathcalorig{M}_{1}$).

Figure 2. Performance of Loopy instantiated with different LLMs, with $15$
completions and prompt $\mathcalorig{M}_{2}$

###  4.2. [RQ2] LLMs generating ingredients of invariant

For RQ2, we experiment with Loopy while using Houdini but not the Repair
procedure. The results are shown as the solid lines of Figure 1. Success rate
for $k<15$ is computed as follows: as an average over randomly sampling $k$
out of the $15$ completions, taking their union and running Houdini.

Houdini has a significant positive impact on the performance of Loopy. With
$15$ completions and the $\mathcalorig{M}_{2}$ prompt, the use of Houdini
increases success rate by 30.7% (from 293 to 383 solved benchmarks). Prompt
$\mathcalorig{M}_{2}$ again does better over $\mathcalorig{M}_{1}$ (327 to 383
solved benchmarks). We can thus conclude from these experiments that LLMs are
much better at finding ingredients of loop invariants than they are at finding
the complete set of invariants. Furthermore, including instructions in the LLM
prompt helps improve accuracy.

Figure 3. Intersection of benchmarks verified by Loopy (with Houdini, without
Repair), using different LLMs

###  4.3. [RQ3] Comparing different LLMs

Results for Loopy without Repair, as we vary the LLM are shown in Figure 2.
Number of completions used for this experiment was fixed at $15$. GPT-4 shows
a superior performance compared to the other models, although GPT-3.5-Turbo is
a close second with 370 solved benchmarks when using Houdini. Interestingly,
using Houdini helps other models “catch up” with GPT-4 by significantly
increasing their success rates.

Figure 3 shows the intersection among the benchmarks verified using the
different LLMs. GPT-4 has the most number of exclusively-solved benchmarks.
GPT-3.5-Turbo is able to solve several cases that GPT-4 could not. Using
multiple LLMs can be beneficial for Loopy.

###  4.4. [RQ4] Using LLMs to fix incorrect invariants

To answer RQ4, we use the full Loopy algorithm, i.e., when using both Houdini
as well as the Repair procedures. Since Loopy with GPT-4 performs the best in
comparison with the other LLMs, we restrict this experiment to GPT-4. For the
same reason, we pick prompt $\mathcalorig{M}_{2}$.

With using Repair, we must decide on the relative budget between generation
and repair. Loopy can be configured with number of completions
$\mathcalorig{N}_{s}$ used for generation and the number of iterations of the
repair loop $\mathcalorig{N}_{r}$ (see Algorithm 1). For a fair comparison we
should have $\mathcalorig{N}_{s}+\mathcalorig{N}_{r}=15$ so that the use of
Repair does not increase the number of LLM responses for Loopy. Since the
performance of Loopy-without-Repair starts to plateau at around $8$
completions (Figure 1), we set $\mathcalorig{N}_{s}=8$ and
$\mathcalorig{N}_{r}=7$. In this case, our evaluation shows that Loopy-with-
Repair verifies an additional 15 benchmarks compared to Loopy-without-Repair.
This implies a total of 398 solved benchmarks.

Consider the program in Example 1. To verify this program, Loopy initially
generates the invariant conjuncts shown in Example 1.1. The conjuncts in bold
capture the behaviour of $x$ and $y$ after the first iteration of the loop.
However, there is no expression that captures the program behaviour before the
loop begins (where $y$ is unconstrained). Upon invoking the Repair procedure,
Loopy generates the invariant shown in Example 1.2 in the fourth repair try.
This invariant allows $y$ to take any value at loop entry, while still
capturing the loop behaviour. This invariant is inductive and sufficient for
verification.

⬇

1void main()

2{

3 int x = 1;

4 int y;

5

6 while (x <= 10)

7 {

8 y = 10 - x;

9 x = x + 1;

10 }

11

12 assert(y < 10);

13}

Ex. 1: Repairing incorrect invariants

$(1\leq x\leq 11)\land(y=10-x)\land\\\ (0\leq y\leq
9)\land(\mathbf{\boldsymbol{y=10-(x-1)}})\land\\\
(\mathbf{\boldsymbol{y<10}})$

Ex. 1.1. Invariant before repair

$(x=1\lor\mathbf{\boldsymbol{y=10-x+1}})\land\\\
(x=1\lor\mathbf{\boldsymbol{y<10}})$

Ex. 1.2. Invariant after repair

###  4.5. [RQ5] Qualitative analysis of the failure cases

To answer RQ5, we consider the benchmarks that remain unverified even with the
repair procedure. We examined these programs and manually came up with the
simplest set of loop invariants that we could find. (The notion of “simple”
here is subjective.) Observing these invariants, we classified the failed
benchmarks into five categories based on the ground truth invariant (which may
not be unique.) The classification can be found in Table 2. The classification
is not indicative of features that are beyond LLMs today; there are also
benchmarks in each of these category that LLMs are able to solve. We do
believe, however, that these feature are somewhat predictive of programs that
LLMs find difficult to reason about.

The first category of failure cases are benchmarks that require disjunctions
in the invariant. These benchmarks can be described as either having loops
with multiple phases (i.e., the code path taken inside the loop body changes
several times, based on flags or other branches, as the loop continues to
iterate), or assertions that depend on whether the loop will be entered or not
(i.e., one needs a disjunct to account for the case that the loop may not
execute even once). The program in Example 2 has a multi-phase loop. It starts
with $x$ and $y$ both at 0; then both increase by 1 in each iteration until
$x$ reaches 50, after which $x$ continues to increase by 1 while $y$ starts to
decrease. Describing these “phases” requires clauses, one for each phase,
connected by disjunctions

The second category of failure cases are benchmarks whose ground truth
invariants requires a clause with at least three variables. An example of an
invariant in this category is the following:
$(0<p)\wedge(2*ielen+leader\\_len\leq bufsize\\_0)\wedge(p=leader\\_len+2*i)$.

The third category of failures are benchmarks where more precise constraints
were required, compared to what was generated by Loopy. For instance, Loopy
finds the invariant $(k=x+y+z)\land(x\leq y)\land(y=z)$ for the benchmark in
Example 3. While this invariant is inductive, it is not sufficient to prove
the assertion. If only the second clause were more precise, claiming $x=y$,
the benchmark would have been verified.

The fourth category requires reasoning about floating point arithmetic. It was
hard to us, even manually, to come up with their ground-truth invariants.

The final category of failures is due to issues in Frama-C. In these cases,
Loopy came up with a correct set of invariants, but Frama-C rejected them,
likely due to imprecise reasoning inside the solver. We believe that it should
be possible to strengthen Frama-C to handle these cases because the reasoning
required is very much within reach of modern SMT solvers. (Some of the
invariants, for instance, required reasoning with integer mod operation that
is supported by solvers like Z3.)

Category | No. of benchmarks
---|---
Ground truth invariant requires disjunctions | 44
Ground truth invariant requires long clauses | 5
Ground truth invariant requires more precise constraints | 9
Ground truth invariant requires floating point reasoning | 3
Frama-C failure | 10
Table 2. Qualitative analysis of the failed benchmarks

⬇

1int main()

2{

3 int x = 0, y = 0, flag = 0;

4 while (flag < 1) {

5 if (y < 0)

6 flag = 1;

7

8 if (flag < 1)

9 x = x + 1;

10

11 if (x < 50)

12 y = y + 1;

13 else

14 y = y - 1;

15 }

16 assert(y == -2 && x == 99);

17 return 0;

18}

Ex. 2: Requires disjunction

⬇

1void main()

2{

3 int x = 0;

4 int y = 0;

5 int z = 0;

6 int k = 0;

7

8 while (unknown_int())

9 {

10 if (k % 3 == 0)

11 {

12 x++;

13 }

14 y++;

15 z++;

16 k = x + y + z;

17 }

18

19 assert(x == y && y == z);

20}

Ex. 3: Requires more precise constraints

###  4.6. [RQ6] Symbolic baseline

We compare the performance of Loopy (with Houdini as well as Repair) against
Ultimate. Overall, Ultimate is able to solve more benchmarks (430 out of 469)
compared to Loopy (398 out of 469). However, there are several benchmarks that
only Loopy can solve, demonstrating that LLMs have the potential of improving
state-of-the-art in program verification. Consider the program in Example 4.
The assertion in line 12 can be verified using the loop invariant $x+y=n$ for
the while loop. Loopy successfully finds this loop invariant while Ultimate
fails to do so. Similarly in Example 5, the loop invariant $k\leq
1000000\>\land\>k\leq i$ can be used to verify the program. Loopy successfully
finds this, but Ultimate does not. Figure 4 shows a comparison between Loopy
and Ultimate. Loopy is able to solve $31$ benchmarks on which Ultimate failed.

⬇

1int main()

2{

3 unsigned int n = unknown_uint();

4 unsigned int x = n, y = 0;

5

6 while (x > 0)

7 {

8 x\--;

9 y++;

10 }

11

12 assert(y == n);

13 return 0;

14}

Ex. 4: Loopy succeeds but Ultimate fails

⬇

1int main()

2{

3 int i = 0;

4 int k = 0;

5

6 while (i < 1000000)

7 {

8 int j = unknown_int();

9 if (!(1 <= j && j < 1000000))

10 return 0;

11 i = i + j;

12 k++;

13 }

14

15 assert(k <= 1000000);

16 return 0;

17}

Ex. 5: Loopy succeeds but Ultimate fails Figure 4. Intersection of benchmarks
verified using Loopy and Ultimate

##  5\. Related work

The success of LLMs in the domain of code-generation tasks (copilot, ;
copilotx, ; codewhisperer, ) has raised interest in applying them towards code
reasoning tasks as well. With a focus on program verification, this naturally
leads to the question of synthesizing invariants for programs.

Pei et al. (pei2023can, ) study this problem by building dataset of programs
and corresponding invariants and then fine-tune a pre-trained LLM on this
dataset. Our approach does not rely on pre-training and directly evaluates the
capabilities of foundational models. Furthermore, Pei et al. do not focus on
generating inductive invariants that are necessary for establishing a formal
proof of correctness.

Chakraborty et al. (chakraborty2023ranking, ) study the problem of
automatically ranking invariants that are generated by an LLM. Their approach,
iRank, builds a custom model for ranking candidate invariants. iRank is
orthogonal and complementary to our work; we can use it as a heuristic for
decreasing the number of calls to the oracle by only checking highly-ranked
invariant candidates. Their approach for candidate invariant generation does
not consider Houdini and do not leverage LLMs for repairing invariants.
Further, iRank uses a lower level SMT-encoding of the input programs. We query
LLMs with C programs instead, arguably a syntax that LLMs should understand
better.

##  6\. Conclusion

This paper evaluates the capabilities of pre-trained Large Language Models
towards unlocking the potential of formal verification. Towards this quest, we
define and evaluate latest LLMs on the task of generating inductive invariants
for program loops. We present a dataset and a toolchain for evaluation. Our
results show that a simple and efficient combination of LLMs with formal
pruning (Houdini) is able to out-perform state-of-the-art symbolic verifiers
on multiple benchmarks. Our results should inspire further research in
combining formal verification and LLMs.

## References

  * (1) Alur, R., Bodik, R., Juniwal, G., Martin, M. M., Raghothaman, M., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., and Udupa, A. Syntax-guided synthesis.  IEEE, 2013.
  * (2) Amazon.  Amazon codewhisperer.  https://aws.amazon.com/codewhisperer/, 2023.
  * (3) Ball, T., Majumdar, R., Millstein, T. D., and Rajamani, S. K. Automatic predicate abstraction of C programs.  In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001 (2001), M. Burke and M. L. Soffa, Eds., ACM, pp. 203–213.
  * (4) Barnett, M., Chang, B. E., DeLine, R., Jacobs, B., and Leino, K. R. M. Boogie: A modular reusable verifier for object-oriented programs.  In Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures (2005), F. S. de Boer, M. M. Bonsangue, S. Graf, and W. P. de Roever, Eds., vol. 4111 of Lecture Notes in Computer Science, Springer, pp. 364–387.
  * (5) Barrett, C., Fontaine, P., and Tinelli, C. The Satisfiability Modulo Theories Library (SMT-LIB).  www.SMT-LIB.org, 2016.
  * (6) Barrett, C. W., Conway, C. L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., and Tinelli, C. CVC4.  In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings (2011), G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806 of Lecture Notes in Computer Science, Springer, pp. 171–177.
  * (7) Beyer, D. Competition on software verification and witness validation: Sv-comp 2023.  In Tools and Algorithms for the Construction and Analysis of Systems (2023), Springer Nature Switzerland, pp. 495–522.
  * (8) Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., and Rival, X. A static analyzer for large safety-critical software.  In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (New York, NY, USA, 2003), PLDI ’03, Association for Computing Machinery, p. 196–207.
  * (9) Brockschmidt, M., Chen, Y., Kohli, P., Krishna, S., and Tarlow, D. Learning shape analysis.  In Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings (2017), F. Ranzato, Ed., vol. 10422 of Lecture Notes in Computer Science, Springer, pp. 66–87.
  * (10) Chakraborty, S., Lahiri, S. K., Fakhoury, S., Musuvathi, M., Lal, A., Rastogi, A., Senthilnathan, A., Sharma, R., and Swamy, N. Ranking llm-generated loop invariants for program verification.  In Findings of The 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP-findings 2023) (2023).
  * (11) Chen, M., Tworek, J., Jun, H., Yuan, Q., de Oliveira Pinto, H. P., Kaplan, J., Edwards, H., Burda, Y., Joseph, N., Brockman, G., Ray, A., Puri, R., Krueger, G., Petrov, M., Khlaaf, H., Sastry, G., Mishkin, P., Chan, B., Gray, S., Ryder, N., Pavlov, M., Power, A., Kaiser, L., Bavarian, M., Winter, C., Tillet, P., Such, F. P., Cummings, D., Plappert, M., Chantzis, F., Barnes, E., Herbert-Voss, A., Guss, W. H., Nichol, A., Paino, A., Tezak, N., Tang, J., Babuschkin, I., Balaji, S., Jain, S., Saunders, W., Hesse, C., Carr, A. N., Leike, J., Achiam, J., Misra, V., Morikawa, E., Radford, A., Knight, M., Brundage, M., Murati, M., Mayer, K., Welinder, P., McGrew, B., Amodei, D., McCandlish, S., Sutskever, I., and Zaremba, W. Evaluating large language models trained on code, 2021.
  * (12) Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. Counterexample-guided abstraction refinement for symbolic model checking.  J. ACM 50, 5 (2003), 752–794.
  * (13) Conchon, S., Coquereau, A., Iguernlala, M., and Mebsout, A. Alt-Ergo 2.2.  In SMT Workshop: International Workshop on Satisfiability Modulo Theories (Oxford, United Kingdom, July 2018).
  * (14) Cousot, P., and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (New York, NY, USA, 1977), POPL ’77, Association for Computing Machinery, p. 238–252.
  * (15) de Moura, L., and Bjørner, N. Z3: An efficient smt solver.  In Tools and Algorithms for the Construction and Analysis of Systems (Berlin, Heidelberg, 2008), C. R. Ramakrishnan and J. Rehof, Eds., Springer Berlin Heidelberg, pp. 337–340.
  * (16) Flanagan, C., and Leino, K. R. M. Houdini, an annotation assistant for esc/java.  In Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity (Berlin, Heidelberg, 2001), FME ’01, Springer-Verlag, p. 500–517.
  * (17) Garg, P., Neider, D., Madhusudan, P., and Roth, D. Learning invariants using decision trees and implication counterexamples.  In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016 (2016), R. Bodík and R. Majumdar, Eds., ACM, pp. 499–512.
  * (18) GitHub.  Github copilot.  https://github.com/features/copilot, 2022.
  * (19) GitHub.  Github copilot-x.  https://github.com/features/preview/copilot-x, 2023.
  * (20) Heizmann, M., Chen, Y.-F., Dietsch, D., Greitschus, M., Hoenicke, J., Li, Y., Nutz, A., Musa, B., Schilling, C., Schindler, T., and Podelski, A. Ultimate automizer and the search for perfect interpolants.  In Tools and Algorithms for the Construction and Analysis of Systems (2018), D. Beyer and M. Huisman, Eds., Springer International Publishing, pp. 447–451.
  * (21) Hoare, C. A. R. An axiomatic basis for computer programming.  Communications of the ACM 12, 10 (1969), 576–580.
  * (22) Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., and Yakobowski, B. Frama-c: A software analysis perspective.  Formal Aspects Comput. 27, 3 (2015), 573–609.
  * (23) Madhukar, K., Wachter, B., Kroening, D., Lewis, M., and Srivas, M. Accelerating invariant generation.  In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design (Austin, Texas, 2015), FMCAD ’15, FMCAD Inc, p. 105–111.
  * (24) McMillan, K. L. Interpolation and sat-based model checking.  In Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings (2003), W. A. H. Jr. and F. Somenzi, Eds., vol. 2725 of Lecture Notes in Computer Science, Springer, pp. 1–13.
  * (25) OpenAI.  GPT-3.5.  https://platform.openai.com/docs/models/gpt-3-5, 2023.
  * (26) OpenAI.  GPT-4 technical report.  https://doi.org/10.48550/arXiv.2303.08774, 2023.
  * (27) Padhi, S., Sharma, R., and Millstein, T. D. Data-driven precondition inference with learned features.  In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016 (2016), pp. 42–56.
  * (28) Pei, K., Bieber, D., Shi, K., Sutton, C., and Yin, P. Can large language models reason about program invariants?  In Proceedings of the 40th International Conference on Machine Learning (2023), ICML’23.
  * (29) Ryan, G., Wong, J., Yao, J., Gu, R., and Jana, S. Cln2inv: Learning loop invariants with continuous logic networks.  In International Conference on Learning Representations (2020).
  * (30) Si, X., Dai, H., Raghothaman, M., Naik, M., and Song, L. Learning loop invariants for program verification.  Advances in Neural Information Processing Systems 31 (2018).
  * (31) Si, X., Naik, A., Dai, H., Naik, M., and Song, L. Code2inv: A deep learning framework for program verification.  Computer Aided Verification 12225 (2020), 151 – 164.
  * (32) Signoles, J., Desloges, B., and Vorobyov, K. E-ACSL User Manual.
  * (33) SVCOMP.  Competition on software verification.  https://sv-comp.sosy-lab.org/.
  * (34) SyGuS-Comp.  Syntax-guided synthesis competition.  https://sygus-org.github.io.
  * (35) Touvron, H., Martin, L., Stone, K., Albert, P., Almahairi, A., Babaei, Y., and et al. Llama 2: Open foundation and fine-tuned chat models.  CoRR abs/2307.09288 (2023).
  * (36) Yao, J., Ryan, G., Wong, J., Jana, S., and Gu, R. Learning nonlinear loop invariants with gated continuous logic networks.  In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (2020), pp. 106–120.
  * (37) Zhu, H., Magill, S., and Jagannathan, S. A data-driven chc solver.  In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (New York, NY, USA, 2018), PLDI 2018, Association for Computing Machinery, p. 707–721.

##  Appendix A Appendix

###  A.1. Prompts and parameters

We set the sampling temperature to $0.7$ and max tokens in one generation to
$2000$ for all queries made to the LLM. The prompts $\mathcalorig{M}_{1}$ and
$\mathcalorig{M}_{2}$ are given below.

Prompt $\mathcalorig{M}_{1}$:  Consider the following C program:
```
{{ code }}
```
Output the loop invariants for the loop in the program above.
Output all the loop invariants in one code block. For example:
```
/*@
loop invariant i1;
loop invariant i2;
*/
```

Prompt $\mathcalorig{M}_{2}$ You are a helpful AI software assistant that
reasons about how code behaves. Given a program, you can find loop invariants,
which can then be used to verify some property in the program. Frama-C is a
software verification tool for C programs. The input to Frama-C is a C program
file with ACSL (ANSI/ISO C Specification Language) annotations. For the given
program, find the necessary loop invariants of the while loop to help Frama-C
verify the post-condition. Instructions: • Make a note of the pre-conditions
or variable assignments in the program. • Analyze the loop body and make a
note of the loop condition. • Output loop invariants that are true (i) before
the loop execution, (ii) in every iteration of the loop and (iii) after the
loop termination, such that the loop invariants imply the post condition. • If
a loop invariant is a conjunction, split it into its parts. • Output all the
loop invariants in one code block.
For example:
```
/*@
loop invariant i1;
loop invariant i2;
*/
``` Rules: • **Do not use variables or functions that are not declared in the
program.** • **Do not make any assumptions about functions whose definitions
are not given.** • **All undefined variables contain garbage values. Do not
use variables that have garbage values.** • **Do not use keywords that are not
supported in ACSL annotations for loops.** • **Variables that are not
explicitly initialized, could have garbage values. Do not make any assumptions
about such values.** • **Do not use the \at(x, Pre) notation for any variable
x.** • **Do not use non-deterministic function calls.**
Consider the following C program:
```
{{ code }}
``` You are allowed to use implication to take care of the conditional nature
of the code. Use implication (==¿) instead of using if-then. For all
variables, add conjunctions that bound the maximum and minimum values that
they can take, if such bounds exist. If a variable is always equal to or
smaller or larger than another variable, add a conjunction for their relation.
If the assertion is guarded by a condition, use the guard condition in an
implication. If certain variables are non-deterministic at the beginning or
end of the loop, use an implication to make the invariant trivially true at
that location. Output the loop invariants for the loop in the program above.
Let’s think step by step.

The prompt, $\mathcalorig{M}_{r}$, used in the Repair procedure is as follows:

You are a helpful AI software assistant that reasons about how code behaves.
Given a program, find loop invariants or fix incorrect invariants, which can
then be used to verify the assertion(s) in the program. Frama-C is a software
verification tool for C programs. The input to Frama-C is a C program file
with ACSL (ANSI/ISO C Specification Language) annotations. For the given
program with loop invariants and the output from Frama-C, fix the invariants
that are not inductive or have syntax errors, so that the program can be
verified. Instructions: • Make a note of the pre-conditions or variable
assignments in the program. • Analyze the loop body and make a note of the
loop condition. • For each invariant that has syntax errors, fix the syntax
errors and ensure that ACSL syntax is followed. • For each invariant that is
not inductive, there are four possibilities: – The invariant is partially
proven to be inductive: In this case, try to fix the non-inductive invariants
that this invariant depends on. – The invariant is preserved but not
established: In this case, add a clause to the invariant such that the new
invariant holds before the loop execution. – The invariant is established but
not preserved: In this case, add a clause to the invariant such that the new
invariant holds after a loop iteration if it holds before the loop iteration.
– The invariant is neither established nor preserved: In this case, remove it
or replace it with a different inductive invariant, or add clauses to the
invariant such that the new invariant is established and preserved. • Finally
output loop invariants that are true (i) before the loop execution, (ii) in
every iteration of the loop and (iii) after the loop termination, such that
the loop invariants can be used to prove the assertion(s) that are labeled as
”Unproven” by Frama-C. • If a loop invariant is a conjunction, split it into
its parts. • Output all the loop invariants in one code block. For example:
```
/*@
loop invariant i1;
loop invariant i2;
*/
```
Rules: • **All undefined variables contain garbage values. Do not use
variables that have garbage values.** • **Do not make assumptions about the
values returned by non-deterministic function calls.** • **Do not use
variables or functions that are not declared in the program.** • **Do not make
any assumptions about functions whose definitions are not given.** • **Do not
use keywords that are not supported in ACSL annotations for loops.** • **Use
\at(x, LoopEntry), instead of \at(x, Pre) to refer to the value of a variable
x just before the beginning of loop execution.** • **Variables that are not
explicitly initialized, could have garbage values. Do not make any assumptions
about such values.** Consider the following program with loops annotated with
the respective loop invariants:
```
{{ code }}
```
Frama-C returns the following message:
```
{{ error }}
```
If the error message indicates a syntax error in the loop annotation, fix the
line with the syntax error. If the error message says ”unbound logic variable
x”, it means that the variable x is not accessible at the location specified
in the loop annotation. If an invariant is partially proven to be inductive,
it means that the verifier is able to prove that the invariant is inductive,
under the assumption that the other invariants are inductive. But some of the
other invariants are not inductive.
If an invariant is established, it means that the verifier is able to prove
that the invariant holds before the loop.
If an invariant is preserved, it means that the verifier is able to prove that
the invariant holds after the loop, assuming that it holds before the loop. To
fix the non-inductive invariants, try the following: If an invariant is
partially proven to be inductive, make sure it is actually inductive. If it is
not, remove it or replace it with a different inductive invariant. If it is,
then fix the other non-inductive invariants.
If an invariant is preserved but not established, add a clause to the
invariant to make it established (a clause that makes the invariant hold
before the loop begins).
If an invariant is established but not preserved, add a clause to the
invariant to make it preserved (a clause that makes the invariant hold after
the loop ends, assuming that it holds before the loop begins).
If an invariant is neither established nor preserved, remove it or replace it
with a different inductive invariant. If none of the above is possible, add a
new loop invariant to strengthen the existing invariants. Please fix all the
above-mentioned errors, and provide the corrected loop invariants for the
program that are sufficient to verify the assertions in the program. Use the
ACSL syntax to specify the invariants. Output only one code block in the end,
with the fixed invariants. **Do not output any other code blocks**. Let’s
think step by step.

###  A.2. Modifications

The important modifications we make to the benchmarks to create our dataset
are as follows:

  * •

Remove all comments - We noticed that some benchmarks had comments about the
loop or the invariant required for verification. To maintain uniformity, we
removed all comments from the benchmarks.

  * •

Replace __VERIFIER_* functions with common functions. Different benchmark
sources use different conventions while referring to function calls with non-
deterministic return values, or calls to their version of an “assume”
function. To maintain uniformity, we replace these calls with calls to
unknown_int(), unknown_float(), etc. for the corresponding non-deterministic
function calls, and use a macro to define assume.

  * •

Convert __VERIFIER_assert() calls to ACSL annotation. Since we use Frama-C as
our oracle, we convert the original assertions in the benchmark to ACSL
annotations, which are comments that are immediately followed by ’@’. For
example, //@ assert().

  * •

Convert Error label statements and reach_error() calls to ACSL. Some
benchmarks contain an error-labeled statement or a reach_error() function
call, with the intention that it should be unreachable in the program. In such
cases, we replace the said statements with //@ assert (\false).

  * •

Fix main function. In some benchmarks, the main function does not return a
value whose type matches the function’s signature. Either a different value is
returned or no value at all. This might be acceptable to most standard C
compilers because they assign some default behaviour in such cases, but
Frama-C returns an error. In order to avoid this, we add a default return
statement that matches the return type of the function. This does not affect
the verification task.

  * •

Pre-processor lines. Some benchmarks might contain lines that are the result
of the program file being passed through a pre-processor. We discard such
lines since they are of no significant meaning for the verification task.