Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class FactSum {
    public static int factorial(int n){
	if (n <=0) return 1;
	else return n*factorial(n-1);    
    }

    public static int doSum(int n){
	int s=0;
	while (n >= 0) {
	    s = s + factorial(n);
	    n=n-1;
	}
	return s;
    }

    public static void main(String[] args) {
	doSum(10);
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE