University of Konstanz
Graduiertenkolleg / PhD Program
Computer and Information Science

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