Program Synthesis for Termination Analysis


Thomas Ströder, LuFG Informatik 2

Title Program Synthesis for Termination Analysis
When 02.09.2010, 15:00
Where Lecture Room Informatik 11
Abstract Termination analysis has been widely studied for a number of special programming languages with simple mathematical definitions like, e.g., term rewriting or definite logic programming. However, there remain many problems when adapting these results to languages like Prolog or C used in real applications. In this talk, we propose a methodology to tackle this challenge. Given a program in a complex language like Prolog or C, we automatically synthesize a corresponding program in a simple language like term rewriting or definite logic programming, such that termination of the synthesized “simple” program implies termination of the original “complex” program. Here, the challenge is to synthesize programs that are suitable for existing automated termination analysis tools. Our approach is based on so-called termination graphs which model the control flow and the side effects of complex languages.