Software Verification Using k-Induction

Extended version of SAS paper with appendix, and technical report

Here is an extended version of the SAS 2011 paper, including proofs.

There is a reference to a technical report on split-case k-induction, available here.

K-Boogie tool and benchmarks

Download and installation

We provide our extension K-Boogie of the Boogie verification back-end.

Our extension is provided in this archive. The archive contains Boogie binaries modified to use the k-induction rule instead of the normal Boogie loop rule, as well as a corresponding altered version of Dafny. The source code of our modifications is provided in form of a patch against SVN version 60898 of Boogie.

K-Boogie is only supported under Windows.

To run K-Boogie, first unpack the above archive. Then download version 2.15 of the Z3 SMT solver (not that it is important to download this specific version). Copy all files contained in the bin directory of the Z3 installation into the k-boogie/Binaries directory. Then you must either add the k-boogie/Binaries directory to your PATH, or explicitly invoke the tool from this directory.

K-Boogie can then be invoked just like Boogie (see the Boogie website for further information). k-Induction is switched on using the command-line option /kInduction:<k>, where <k> >= 0 is the default value to be used for loop unwinding.

To specify the unwinding depth on a per-loop basis (overriding the default <k> specified using the /kInduction switch), the directive kUnwind <k>; can be used within Boogie programs:

  while (true)
    invariant !IsHeld(mutex);
    kUnwind 1;
  {
    // ...
  }

For questions about K-Boogie contact alastair.donaldson@comlab.ox.ac.uk or philipp.ruemmer@it.uu.se.

Running K-Boogie on a simple example

Consider the following simple Boogie procedure, which is similar to the running example used in the SAS paper:

procedure Rotate(N : int) returns (x : int)
  ensures x == 0;
{

  var a : int, b : int, c : int, i : int, temp : int;

  a := 1;
  b := 2;
  c := 3;
  x := 0;

  i := 0;

  while(i < N) {
   assert(a != b);
   temp := a;
   a := b;
   b := c;
   c := temp;
   i := i+1;
  }

}

Standard Boogie cannot verify this program correct without any loop invariant being supplied. This is demonstrated by running K-Boogie on the example without k-induction:

Boogie.exe Rotation.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.
Rotation.bpl(15,5): Error BP5001: This assertion might not hold.
Execution trace:
  Rotation.bpl(7,5): anon0
  Rotation.bpl(14,3): anon2_LoopHead
  Rotation.bpl(15,5): anon2_LoopBody

Boogie program verifier finished with 0 verified, 1 error

However, the program can be verified without any additional invariants if k-induction is used, with k=3:

Boogie.exe /kInduction:3 Rotation.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.

Boogie program verifier finished with 1 verified, 0 errors

Verification does not succeed with smaller values of k.

Verifying bubble sort with weaker invariants

The rotation example is contrived to illustrate the strengths of k-induction. We now turn to a more realistic example, an implementation of bubble sort provided with the Boogie distribution. This is availalbe from the archive of benchmarks below, as Bubble.bpl

First, we see that the original Boogie program can be verified without k-induction, as sufficient invariants are supplied:

Boogie.exe Bubble.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.

Boogie program verifier finished with 1 verified, 0 errors

If we comment out the following invariant at line 54:

invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);

we see that Boogie cannot directly verify the example:

Boogie.exe Bubble.bpl
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.
Bubble.bpl(61,7): Error BP5003: A postcondition might not hold on this return path.
Bubble.bpl(30,3): Related location: This is the postcondition that might not hold.
Execution trace:
  Bubble.bpl(36,5): anon0
  Bubble.bpl(37,3): anon9_LoopHead
  Bubble.bpl(37,3): anon9_LoopDone
  Bubble.bpl(46,3): anon10_LoopHead
  Bubble.bpl(59,7): anon10_LoopBody
  Bubble.bpl(61,7): anon11_Then
Bubble.bpl(72,7): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
  Bubble.bpl(36,5): anon0
  Bubble.bpl(37,3): anon9_LoopHead
  Bubble.bpl(37,3): anon9_LoopDone
  Bubble.bpl(46,3): anon10_LoopHead
  Bubble.bpl(59,7): anon10_LoopBody
  Bubble.bpl(60,5): anon11_Else

Boogie program verifier finished with 0 verified, 2 errors

However, if 1-induction is used, verification succeeds:

Boogie.exe Bubble.bpl /kInduction:1
Boogie program verifier version 2.0.0.0, Copyright (c) 2003-2010, Microsoft.

Boogie program verifier finished with 1 verified, 0 errors

This demonstrates the usefulness of k-induction in the verification of general-purpose examples.

Benchmarks used in the SAS paper

The K-Boogie benchmarks used in our paper are derived from test-cases and benchmarks shipped with the standard version of Boogie.

K-Boogie is applied to each benchmark using command lines similar to those in the above examples, except that the additional command-line argument /proc:<p> is used to analyse procedure <p> of a program in isolation.

K-Inductor tool and benchmarks

K-Inductor is a k-induction-based verifier for ANSI C programs, built on top of the CBMC tool.

Download and installation

K-Inductor is currently available for 64-bit x86 Linux platforms: kinductor-0.1-linux-x86-64.tar.gz. Versions for other platforms are available on request.

K-Inductor uses MiniSat 2 as a back-end SAT solver. You do not need to download MiniSat; it is part of the kinductor executable.

After downloading and unzipping the archive, put kinductor on your PATH and you are ready to go.

You should also read the license.

Running K-Inductor on a simple example

Consider the following C variant of the rotation example:

int rotate(int N)
{
  int a, b, c, x, i, temp;
  a = 1;
  b = 2;
  c = 3;
  x = 0;

  for(i = 0; i < N; i++)
  {
    __CPROVER_k_induction_hint(3,3,0,0);
    assert(a != b);
    temp = a;
    a = b;
    b = c;
    c = temp;
  }

  assert(x == 0);

}

The statement __CPROVER_k_induction_hint(3,3,0,0) tells K-Inductor how k-induction should be applied to the closest loop containing the statement. It has no executable effect. The first two parameters specify the minimum and maximum values of k to be tried; the third specifies the amount by which k should be incremented if verification is unsuccessful (here this is zero, since the minimum and maximum values are the same). The final parameter is related to a work-in-progress addition, and should currently always be set to zero. If no hint is provided for a given loop, a default hint __CPROVER_k_induction_hint(0,0,1,0) is used.

We run K-Inductor on this example, assuming that it is in file example.c, as follows: kinductor --function rotate example.c

This generates the following output (which has been trimmed a bit):

Type-checking example
Generating GOTO Program
Generic Property Instrumentation
Cutting loop headed at line 11 with k = 3
Cutting complete!
The program does not have any loops, so BMC will be applied.
Starting Bounded Model Checking
size of program expression: 103 assignments
simple slicing removed 34 assignments
Generated 5 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
1568 variables, 4614 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.018s
VERIFICATION SUCCESSFUL

Thus k=3 is sufficient to verify correctness of this example. To see that k=2 is not sufficient, change __CPROVER_k_induction_hint(3,3,0,0) to:

__CPROVER_k_induction_hint(2,2,0,0)

Split-case k-induction

By default, K-Inductor applies the combined-case k-induction method described in the SAS paper. It also supports split-case k-induction, which, as discussed in the submission, is less powerful. To try split-case k-induction on the above example, do:

kinductor --function rotate example.c --split-case

You should find that verification fails, no matter how large a value of k is used. (Technically, setting k to be larger than the maximum possible integer should allow verification to succeed, but this is clearly infeasible.)

If the line assert(x == 0) is commented out, then split-case k-induction can verify the example using k=3. The reasons for this are discussed in the SAS paper.

Benchmarks used in the SAS paper

In the SAS paper, we apply K-Inductor to a set of DMA processing benchmarks for the Cell BE processor, taken from the IBM Cell SDK.

The benchmarks were also studied in previous work in a TACAS 2010 paper, in which further details can be found.

For this purpose, K-Inductor is embedded in the Scratch tool, which automatically instruments programs involving DMA operations with assertions and auxiliary variables to check for races.

To run the benchmarks, please download Scratch: scratch-1.0-linux-x86-64.tar.gz and put the scratch executable on your PATH (please note that you can do this without having downloaded the stand-alone version of K-Inductor described above.

You can download an archive of benchmarks, or browse the benchmarks online.

Inside each benchmark folder are two scripts, run_combined and run_split, which apply Scratch using combined- or split-case k-induction respectively.

In each benchmark, you will see many lines of the form:

INVARIANT(assert(phi));

These are pre-processed away to nothing when combined-case k-induction is used. With split-case k-induction, they are replaced with the enclosed assertion. We demonstrate that combined-case k-induction is stronger than split-case k-induction by the fact that, removing any of these invariants, causes the split-case approach to fail.

Also, there are many lines of the form:

AUXILIARY(x);

Once again, these are pre-processed away when the combined-case method is used. With the split-case method, these statements are necessary to manipulate auxiliary variables associated with strengthening assertions provided via the INVARIANT construct.