Invel - The Automatic Non-Termination-Detection Tool

Invel is a tool for detecting the potential non-termination of Java-programs (as a means of debugging). Think of it as a solution to the halting problem. Invel enriches the theorem prover KeY with an automatic invariant generator (for showing that a program never reaches terminating states) and constraint solving (for finding critical inputs).

As an example, imagine that we want to analyse the following program for computing the least common multiple of two integers:

   public static int lcm (int a, int b) {
            int am = a;
            int bm = b;

            while (am != bm) {
                 if (am > bm) {
                       bm = bm+b;
                 } else {
                       am = am+a;
                 }
            }
            return am;
   }

When running Invel on this program, it would determine that:

• All inputs that satisfy the formula a < 1 && a < b are critical,
• For such inputs, the loop preserves the invariant a < b, which implies that the loop never terminates.

Thus, we would have proven that the program is (potentially) non-terminating.

A detailed description of the tool and the theory around it is available. The tool is also introduced in the following paper:

• Helga Velroyen, Philipp Rümmer
  Non-Termination Checking for Imperative Programs
  2nd International Conference on Tests and Proofs, Prato, Italy, 2008
  To appear in LNCS
  (Preliminary PDF - BibTeX - Abstract)
  

Download

• Source distribution of the non-termination checker
  Author: Helga Velroyen, helga-at-velroyen-dot-de
  
  License: GPL 3
  
• Example database of over 50 (non-terminating) programs that were used to test Invel

Please note that all parts of the implementation are very experimental. If things go wrong and the program or the generated invariant eats your cat:

Installation of the Tool (currently only for Linux x86)

1. Install KeY from the distribution above, which works as for the normal version of KeY. It is not necessary to have Borland Together installed.
   If you had ever installed KeY before, you should first remove the directory ~/.key
   
2. Put the program key-invel/system/cooper in some directory that is in the PATH and make sure that it is executable.
3. Build the invariant generator, which is located in the directory key-invel/non-termination, following the README in the same directory.

And this should be it!

Invocation

The usage of Invel is described in key-invel/non-termination/README. If your installation was successful and if you have downloaded the examples from above, then it should be possible to do a non-termination proof as follows:

> java -jar key-invel/non-termination/dist/invel-[...].jar \
       -p [...]/key-invel/bin/runProver \
       -x /usr/bin/xvfb-run \
       -bd [...]/collection.clean/heap/arraySum \
       -kf invel.key -mf modifies.key.stx -sf Sum.java \
       -c all -f all -j all -mi 10 -mc 10

(you have to insert the absolute paths and the right filenames instead of [...])

If the program xvfb-run is not available on your computer and you don't mind that KeY keeps popping up during non-termination proofs, just remove the option -x /usr/bin/xvfb-run.

Options

-h             Shows this help.
-help          Shows this help.
-bd basedir    The directory where the examples are located.
-p filename    The absolute path and filename of the prover.
-x filename    The absolute path and filename of the xvfb-run binary.
-n name        The name of the example directory (subdirectory of basedir).
-kf filename   The filename of the key file. Default: invel.key.
-mf filename   The filename of the modifier file. Default: modifies.key.stx.
-op praefix    A prefix added to the output directory. Useful for naming different runs.
-mi num        Maximum number of iterations. Default: 10
-md num        Maximum depth of invariants. Default: 15
-mn num        Maximum number of nodes of invariants. Default: 50
-c creator1 creator2 ...
               List of fragment creators. Default: all.
-f filter1 filter2 ...
               List of invariant filters. Default: all.
-j judge1 weight1 judge2 weight2 ...
               List of invariant judges. Default: all, equally weighted.

---

In case of problems, you may drop a mail to philipp-at-chalmers-dot-se or helga-at-velroyen-dot-de.