|
|
||
|
IMADA - Department of Mathematics and Computer Science |
|
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. Host: Peter Schneider-Kamp SDU HOME | IMADA HOME | Previous Page Daniel Merkle |