Where does the KeY verification tool shine?

Question

What are some code examples demonstrating KeY’s strength?

Details

With so many Formal Method tools available, I was wondering where KeY is better than its competition, and how? Some readable code examples would be quite helpful for comparison and understanding.

Updates

Searching through the KeY website, I found code examples from the book — is there a suitable code example in there somewhere?

Furthermore, I found a paper about the bug that KeY found in Java 8’s mergeCollapse in TimSort. What is a minimal code from TimSort that demonstrates KeY’s strength? I do not understand, however, why model checking supposedly cannot find the bug — a bit array with 64 elements should not be too large to handle. Are other deductive verification tools just as capable of finding the bug?

Is there an established verification competition with suitable code examples?

Answer 1

This is a very hard question, which is why it hasn't yet been answered after having already been asked more than one year ago (and although we from the KeY community are well aware of it...).

The Power of Interaction

First, I'd like to point out that KeY is basically the only tool out there allowing for interactive proofs of Java programs. Although many proofs work automatically and we have quite powerful automatic strategies at hand, sometimes interaction is required to understand why a proof fails (too weak or even wrong specifications, wrong code or "just" a prover incapacity) and to add suitable corrections or strengthenings.

Feedback from Proof Inspection

Especially in the case of a prover incapacity (specification and program are OK, but the problem is too hard for the prover to succeed automatically), interaction is a powerful feature. Many program provers (like OpenJML, Dafny, Frama-C etc.) rely on SMT solvers in the backend which they feed with many more or less small verification conditions. The verification status for these conditions is then reported back to the user, basically as pass or fail -- or timeout. When an assertion failed, a user can change the program or refine the specifications, but cannot inspect the state of the proof to deduct information about why something went wrong; this style is sometimes called "auto-active" as opposed to interactive. While this can be quite convenient in many cases (especially when proofs pass, since the SMT solvers can be really quick in proving something), it can be hard to mine SMT solver output for information. Not even the SMT solvers themselves know why something went wrong (although they can produce a counterexample), as they just are fed a set of formulas for which they attempt to find a contradiction.

TimSort: A Complicated Algorithmic Problem

For the TimSort proof which you mentioned, we had to use a lot of interaction to make them pass. Take, for instance, the mergeHi method of the sorting algorithm which has been proven by one of the most experienced KeY power users known to me. In this proof of 460K proof nodes, 3K user interactions were necessary, consisting of quite a lot of simple ones like the hiding of distracting formulas, but also of 478 quantifier instantiations and about 300 cuts (on-line lemma introduction). The code of that method features many difficult Java features like nested loops with labeled breaks, integer overflows, bit arithmetic and so on; especially, there are a lot of potential exceptions and other reasons for branching in the proof tree (which is why in addition, also five manual state merging rule applications have been used in the proof). The workflow for proving this method basically was to give the strategies a try for some time, check the proof state afterward, prune back the proof and introduce a helpful lemma to reduce the overall proof work and to start again; occasionally, quantifiers were instantiated manually if the strategies failed to find the right instantiation directly by themselves, and proof tree branches were merged to tackle state explosion. I would just claim here that proving this code is (at least currently) not possible with auto-active tools, where you cannot guide the prover in that way, and also cannot obtain the right feedback for knowing how to guide it.

Strength of KeY

Concluding, I'd say that KeY's strong in proving hard algorithmic problems (like sorting etc.) where you have complicated quantified invariants and integer arithmetic with overflows, and where you need to find quantifier instantiations and small lemmas on the fly by inspecting and interacting with the proof state. The KeY approach of semi-interactive verification also excels in general for cases where SMT solvers time out, such that a user cannot tell whether something is wrong or an additional lemma is required.

KeY can of course also proof "simple" problems, however there you need to take care that your program does not contain an unsupported Java feature like floating point numbers or multithreading; also, library methods can be quite a problem if they're not yet specified in JML (but this problem applies to other approaches as well).

Ongoing Developments

As a side remark, I also would like to point out that KeY is now more and more being transformed to a platform for static analysis of different kinds of program properties (not only functional correctness of Java programs). On the one hand, we have developed tools such as the Symbolic Execution Debugger which can be used also by non-experts to examine the behavior of a sequential Java program. On the other hand, we are currently busy in refactoring the architecture of the system for making it possible to add frontends for languages different than Java (in our internal project "KeY-RED"); furthermore, there are ongoing efforts to modernize the Java frontend such that also newer language features like Lambdas and so on are supported. We are also looking into relational properties like compiler correctness. And while we already support the integration of third-party SMT solvers, our integrated logic core will still be there to support understanding proof situations and manual interactions for cases where SMT and automation fails.

TimSort Code Example

Since you asked for a code example... I cannot right know think of "the" code example showing KeY's strength, but maybe for giving you a flavor of the complexity of mergeHi in the TimSort algorithm, here a shortened excerpt with some comments (the full method has about 100 lines of code):

private void mergeHi(int base1, int len1, int base2, int len2) {
  // ...
  T[] tmp = ensureCapacity(len2); // Method call by contract
  System.arraycopy(a, base2, tmp, 0, len2); // Manually specified library method

  // ...

  a[dest--] = a[cursor1--]; // potential overflow, NullPointerException, ArrayIndexOutOfBoundsException
  if (--len1 == 0) {
    System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
    return; // Proof branching
  }
  if (len2 == 1) {
    // ...
    return; // Proof branching
  }

  // ...
outer: // Loop labels...
  while (true) {
    // ...
    do { // Nested loop
      if (c.compare(tmp[cursor2], a[cursor1]) < 0) {
        // ...
        if (--len1 == 0)
          break outer; // Labeled break
      } else {
        // ...
        if (--len2 == 1)
          break outer; // Labeled break
      }
    } while ((count1 | count2) < minGallop); // Bit arithmetic

    do { // 2nd nested loop
      // That's one complex statement below...
      count1 = len1 - gallopRight(tmp[cursor2], a, base1, len1, len1 - 1, c);
      if (count1 != 0) {
        // ...
        if (len1 == 0)
          break outer;
      }
      // ...
      if (--len2 == 1)
        break outer;

      count2 = len2 - gallopLeft(a[cursor1], tmp, 0, len2, len2 - 1, c);
      if (count2 != 0) {
        // ...
        if (len2 <= 1)
          break outer;
      }
      a[dest--] = a[cursor1--];
      if (--len1 == 0)
        break outer;
      // ...
    } while (count1 >= MIN_GALLOP | count2 >= MIN_GALLOP);
    // ...
  }  // End of "outer" loop
  this.minGallop = minGallop < 1 ? 1 : minGallop;  // Write back to field

  if (len2 == 1) {
    // ...
  } else if (len2 == 0) {
    throw new IllegalArgumentException(
        "Comparison method violates its general contract!");
  } else {
    System.arraycopy(tmp, 0, a, dest - (len2 - 1), len2);
  }
}

Verification Competition

VerifyThis is an established competition for logic-based verification tools which will have its 7th iteration in 2019. The concrete challenges for past events can be downloaded from the "archive" section of the website I linked. Two KeY teams participated there in 2017. The overall winner that year was Why3. An interesting observation is that there was one problem, Pair Insertion Sort, which came as a simplified and as an optimized Java version, for which no team succeeded in verifying the real-world optimized version on site. However, a KeY team finished that proof in the weeks after the event. I think that highlights my point: KeY proofs of difficult algorithmic problems take their time and require expertise, but they're likely to succeed due to the combined power of strategies and interaction.