Termination Analysis by Learning Terminating Programs
CAV, pp. 797-813, 2014.
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be represented by a finite lasso. The analysis can \"learn\" a program from a termination proof for the lasso, a program that is terminati...More
PPT (Upload PPT)