Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

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

Amir M. Ben-AmramContact Information and Michael CodishContact Information

(1)  School of Computer Science, Tel-Aviv Academic College, Israel
(2)  Department of Computer Science, Ben-Gurion University, Israel
Abstract
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.

Contact Information Amir M. Ben-Amram
Email: amirben@mta.ac.il

Contact Information Michael Codish
Email: mcodish@cs.bgu.ac.il
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.111 • Server: mpweb19
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)