Carsten Fuhs

 

Termination Analysis for Programming Languages using SAT Solving

 

Abstract:

Well-founded orderings are the most basic, but also most important
ingredient to virtually all termination analyses. Orderings based on
polynomial interpretations (POLO) are arguably among the most popular
choices in the termination analysis of term rewrite systems. Numerous
fully automated search algorithms for this class of orderings have
therefore been devised and implemented in termination tools.

Unfortunately, the performance of these algorithms on all but the
smallest termination problems has been lacking. E.g., recently
developed transformations from programming languages like Haskell or
Prolog allow to apply termination tools for term rewrite systems to
real programming languages. The results of the transformations are
often of non-trivial size, though, and cannot be handled efficiently by
the existing algorithms. For example, Constraint Logic Programming
(CLP) is considered to be a very mature approach to solving polynomial
constraints, yet state-of-the-art CLP tools require too much time on
many of our problem instances.

Hence, the need for more efficient search algorithms has triggered
research in reducing the resulting search problems into decision
problems for which more efficient algorithms already exist. Here, we
introduce an encoding of POLO to the satisfiability of propositional
logic (SAT). We implemented this encoding in our termination tool
AProVE. Extensive experiments have shown that one can obtain speedups
in orders of magnitude by this encoding and the application of modern
SAT solvers.

The talk is based on joint work with Jürgen Giesl, Aart Middeldorp,
Peter Schneider-Kamp, René Thiemann, and Harald Zankl.