Inference of polynomial invariants for imperative programs:
a farewell to Gröbner
A companion web page

Additional material

• The INRIA Research Report No.7627 is an earlier version of the submitted article, with additional proofs, examples, and descriptions.
• The proof of equivalence between concrete semantics of Definition 5 and a more clasical small-step operational semantics and the correctness proof of the abstract semantics defined in Figure 2 are collected in a compendium to ease their perusal.
  
• The Coq sheet (tested with Coq 8.3pl2) formalizing the small-step and backwards semantics equivalence. Part of the formalization of our operational semantics is due to Leroy and Grall's Coinductive big-step operational semantics.
  
• An extended version of the article can be found in Chapter 4 of Arnaud Jobin's PhD (in French).
  

Benchmarks and measurements

• Download the Maple sheets (tested with Maple 11). Our tests were run on a 2.8 GHz Intel Core 2 Duo sporting 4 Go of DDR3 RAM.
  

A Caml implementation

We are currently using Sawja, a static analysis framework that targets Java bytecode, to develop a Caml implementation of the analysis. The framework provides facilities to retrieve and manipulate intermediate code representations, which guide the construction of our abstract values.

The annotation Java package

• Use this package to annotate your Java sources files

The fast polynomial invariant generator (last update: 06/25/12)

• An online interface to the typechecker (coming soon).
• The sources of our invariant inference prototype. These require the Javalib/Sawja static analysis libraries to run.

How to use it

• Compile your java source files using our annotation package
• Compile and install our invariant generator.
• Give the classpath, class name, and invariant characteristics to the prototype to perform invariant generation. E.g.

  polyinv --classpath $CLASSPATH --class Example --vars "x:y:z" --deg 2

How to annotate your classes

Simply annotated the method you would like to analyze with @Analyze.

Examples

The Mannadiv class, implementing the division algorithm from Manna's "Mathematical Theory of Computation".

import quantitative.Analyze;

public class Mannadiv {

  @Analyze 
  public static void main(String[] args) {
    int x1, x2, y1, y2, y3;
    x1 = Integer.parseInt(args[0]);
    x2 = Integer.parseInt(args[1]);
    y1 = 0;
    y2 = 0;
    y3 = x1;
    while (y3 != 0) {
      if (x2 == y2 + 1) {
        y1++;
        y2 = 0;
        y3--;
      } else {
        y2++;
        y3--;
      }
      System.out.format("x1 = %d, x2 = %d\ny1 = %d, y2 = %d, y3 = %d\n", x1, x2, y1, y2, y3);
    }
  }
}

The Knuth class, implementing the divisor research algorithm from Knuth's "The Art of Computer Programming, Volume 2".

import quantitative.Analyze;

public class Knuth {

  @Analyze
  public static void main(String[] args) {
    int n, d, r, rp, q, t, n1, n2;
    double s;
    n  = Integer.parseInt(args[0]);
    d  = Integer.parseInt(args[1]);
    n1 = n/d;
    n2 = n/(d-2);
    r  = n - n1 * d;
    rp = n - n2 * (d-2);
    q  = 4 * (n2 - n1);
    s  = Math.sqrt(n);

    while ((s >= d) && (r != 0)) {
      if (2*r-rp+q < 0) {
        t  = r;
        r  = 2*r-rp+q+d+2;
        rp = t;
        q  = q+4;
        d  = d+2;
      } else if ((2*r-rp+q >= 0) && (2*r-rp+q < d+2))  {
        t  = r;
        r  = 2*r-rp+q;
        rp = t;
        d  = d+2;
      } else if ((2*r-rp+q >= 0) && (2*r-rp+q >= d+2) && (2*r-rp+q < 2*d+4)) {
        t  = r;
        r  = 2*r-rp+q-d-2;
        rp = t;
        q  = q-4;
        d  = d+2;
      } else { /* ((2*r-rp+q >= 0) && (2*r-rp+q >= 2*d+4)) */
        t  = r;
        r  = 2*r-rp+q-2*d-4;
        rp = t;
        q  = q-8;
        d  = d+2;
      }
      System.out.format("n = %d, d = %d\nr = %d, rp = %d, q = %d, s = %f, t = %d, n1 = %d, n2 = %d\n", n, d, r, rp, q, s, t, n1, n2);
    }
    System.out.format("Result: d = %d\n", d);
  }
}