Publications
Back to Publications
| Author(s) |
Leue, S., Wei, W. |
| Title |
A region graph based approach to termination proofs |
| Abstract |
Automated termination proofs are indispensable in the mechanic verification
of many program properties. While most of the recent work on automated
termination proofs focuses on the construction of linear ranking functions,
we develop an approach based on region graphs in which regions define subsets
of variable values that have different effects on loop termination. In order to establish
termination, we check whether (1) any region will be exited once it is
entered, and (2) no region is entered an infinite number of times.We show the effectiveness
of our proof method by experiments with Java code using a prototype
implementation of our approach. |
| Download |
LeWe06.pdf |
Back to Publications
|
