CFL-Termination

CFL-reachability is the essence of partial correctness for recursive programs, where the qualifier CFL refers to the stack-based call/return discipline of program executions. Accordingly CFL-termination is the essence of total correctness for recursive programs. In this paper we present a program analysis method for CFL-termination. Until now, we had only program analysis methods for recursion or total correctness, but not both. We use the RHS framework~RepsPOPL95 for interprocedural analysis to show how such methods can be integrated into a practical method for both.