Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class FactSumList {
    static int factorial(int n){
	int fact = 1;
	for (int i=1; i <= n; i++) fact = fact * i;
	return fact;	  
    }

    public static int doSum(ListReverse x){
	if (x==null) return 0;
	else return factorial(x.data) + doSum(x.next);	
    }

    public static void main(String [] args) {
	ListReverse l = new ListReverse();
	l.next = new ListReverse();
	doSum(l);
    }
}


class ListReverse {
    ListReverse next;
    int  data;
    int length;

    public ListReverse listReverse(ListReverse x) {
	ListReverse result = null;
	ListReverse tmp = null;

	while ( x != null ) {
	    tmp = x.next;
	    x.next = result;
	    result = x;
	    x = tmp;
	}

	return result;
    }
   
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE