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.

tr-2008-160.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2008-160
Pages11
InstitutionMicrosoft Research
> Publications > CFL-Termination