Abstract
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 terminating by construction. In a second step, the analysis checks that the set of sample traces is representative in a sense that we can make formal. An experimental evaluation indicates that the approach is a potentially useful addition to the portfolio of existing approaches to termination analysis. © 2014 Springer International Publishing.
Cite
CITATION STYLE
Heizmann, M., Hoenicke, J., & Podelski, A. (2014). Termination analysis by learning terminating programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8559 LNCS, pp. 797–813). Springer Verlag. https://doi.org/10.1007/978-3-319-08867-9_53
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
