Hackeython Working Group: Project Management

Shepard: Daniel

Motivation

Anyone attempting to verify a big(ger) project in KeY, knows the limitation of KeY's current proof/project management. The current proof management view shows which projects in which classes/interfaces has been verified so far---but only for loaded proofs. KeY has no information about unloaded proofs.

This also makes unsound proofs possible. The following two methods can be proven (including termination) by proving m() using the contract of n(), closing KeY and then proving n().

class Problem {
  //@ ensures false;
  void m() { n(); }

  //@ ensures false;
  void n() { m(); }
}

In addition, the lack of management makes it difficult to track what has been proven, which taclet setting have been used, etc.

Idea

In this working group, we explore what KeY's proof and project management should look like, how we can implement it best, etc. The proof management should detect illegal cycles, track settings and source code versions, and list all (partially) proven contracts. Special attention should be taken to make the management usable without a GUI to make KeY easier to use with CI and allow reproducing the results of artifacts.

Possible Discussion Points

• Which features are most important?
• How to implement project management in a backward-compatible way?
• Is this tool an extension or part of KeY?