A SAT-Based Approach to Size Change Termination with Global Ranking Functions

Amir Ben-Amram and Michael Codish   

Fourteenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS); 2008


We describe a new approach to proving termination with size change graphs. This is the first decision procedure for size change termination (SCT) which makes direct use of global ranking functions. It handles a well-defined and significant subset of SCT instances, designed to be amenable to a SAT-based solution. We have implemented the approach using a state-of-the-art Boolean satisfaction solver. Experimentation indicates that the approach is a viable alternative to the complete SCT decision procedure based on closure computation and local ranking functions. Our approach has the extra benefit of producing an explicit witness to prove termination in the form of a global ranking function.

Available:    bibtex entry   pdf

Related sites:   Online Analyzer

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel

© copyright notice