SAT Solving for Termination Analysis with Polynomial Interpretations

Abstract Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.

Authors

• Carsten Fuhs
• Jürgen Giesl
• Aart Middeldorp
• Peter Schneider-Kamp
• René Thiemann
• Harald Zankl

Keywords

No keywords are indexed for this paper.