Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class Node1 implements Node {
    private Node next;
    private int value;

    public Node1(int value, Node next) {
	this.value = value;
	this.next = next;
    }

    public Node getNext() {
	return next;
    }

    public void setNext(Node next) {
	this.next = next;
    }

    public int getValue() {
	return value;
    }

    public void setValue(int value) {
	this.value = value;
    }
}

public class Node2 implements Node {
    private Node next;
    private int value;

    public Node2(int value, Node next) {
	this.value = value;
	this.next = next;
    }

    public Node getNext() {
	return next;
    }

    public void setNext(Node next) {
	this.next = next;
    }

    public int getValue() {
	return value;
    }

    public void setValue(int value) {
	this.value = value;
    }
}

public class Node3 implements Node {
    private Node next;
    private int value;

    public Node3(int value, Node next) {
	this.value = value;
	this.next = next;
    }

    public Node getNext() {
	return next;
    }

    public void setNext(Node next) {
	this.next = next;
    }

    public int getValue() {
	return value;
    }

    public void setValue(int value) {
	this.value = value;
    }
}

public interface Node {
    public Node getNext();
    public void setNext(Node next);
    public int getValue();
    public void setValue(int value);
}

/**
 * Method main() terminates.
 */

public class TestJulia5 {
    public static void main(String[] args) {
	Node last = new Node1(1,null);
	Node n = new Node2(2,last);
	int counter = 0;

	n = new Node1(3,n);
	n = new Node3(4,n);
	n = new Node1(5,n);
	n = new Node2(6,n);
	n = new Node3(7,n);
	last.setNext(n);

	while (n != null && counter++ < last.getValue()) {
	    if (n instanceof Node2)
		n.setValue(n.getValue() + 1);
	    n = n.getNext();
	}
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
TestJulia5.main([Ljava/lang/String;)V: Graph of 172 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE