Term Rewrite System Synthesis for Termination Analysis of C Programs

Speaker

Thomas Ströder

Title Term Rewrite System Synthesis for Termination Analysis of C Programs
When 09.03.2011, 10:00
Where Room 5052
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 C used in real applications.

In this talk, we propose a methodology to tackle this challenge. Given a program in a complex language like C, we automatically synthesize a corresponding program in a simple language like term rewriting, 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.

Slides