Conferences on Intelligent Computer Mathematics - Birmingham 2008
CICM '08

Doctoral Programme

Birmingham, UK, 29-31 July 2008

Rafael Navarro: Termination Analysis with Polynomial Ordering

Termination is an essential property of programs. Although it is in general undecidable, a lot of research has been devoted to discov- ering classes of programs where it is decidable, and to the development of suitable techniques for proving termination in interesting cases. Proofs of termination of programs involve solving constraints between expressions coming from (parts of ) the program. Polynomial interpretations are a standard technique used in almost all tools for proving termination automatically. Traditionally, one uses interpretations with polynomials over the naturals and CSP-like algorithms over finite domain. But recently, it was shown that interpretations with polynomials over the rationals and SAT-based methods can be signi´Čücantly more powerful.However, polynomials over other sets of numbers have not been considered as well as other powerful techniques which are underexplored to date (Linear and Non-Linear Programming, SMT, Domain-Specific SP Solvers, ...).