Summarization for termination: no return! |
| |
Authors: | Byron Cook Andreas Podelski Andrey Rybalchenko |
| |
Affiliation: | 1.Microsoft Research,Cambridge,UK;2.Queen Mary,University of London,London,UK;3.University of Freiburg,Freiburg,Germany;4.Max Planck Institute for Software Systems (MPI-SWS),Saarbrücken,Germany |
| |
Abstract: | We propose a program analysis method for proving termination of recursive programs. The analysis is based on a reduction of
termination to two separate problems: reachability of recursive programs, and termination of non-recursive programs. Our reduction
works through a program transformation that modifies the call sites and removes return edges. In the new, non-recursive program,
a procedure call may non-deterministically enter the procedure body (which means that it will never return) or apply a summary
statement. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|