Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Virtual

public class Div extends Node {
    public int length() {
	return length();
    }
}

public class Internal extends Node {
    private Node next;

    public Internal(Node next) {
	this.next = next;
    }

    public int length() {
	return 1 + next.length();
    }
}

public class Nil extends Node {
    public int length() {
	return 0;
    }
}

public abstract class Node {
    public abstract int length();
}

/**
 * An iteration over a list of <tt>Internal</tt> nodes ending with
 * a terminating node <tt>Nil</tt>.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * This example shows termination in the case of virtual calls
 * to <tt>length()</tt>.
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class Virtual {
    public static void main(String[] args) {
	Node d = new Div();
	Node n = new Nil();
	int l = 28; //Integer.parseInt(args[0]);
	while (l-- > 0) n = new Internal(n);

	n.length();
    }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Virtual.main([Ljava/lang/String;)V: Graph of 709 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE