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.

BibTeX

@inproceedings{FGMSTZ-SAT07,
  author    = "Carsten Fuhs and J{\"u}rgen Giesl and Aart Middeldorp and
               Peter Schneider-Kamp and R{\'e}ne Thiemann and Harald Zankl",
  title     = "{SAT} Solving for Termination Analysis with Polynomial
               Interpretations",
  booktitle = "Proceedings of the 10th International Conference on Theory
               and Applications of Satisfiability Testing",
  series    = "Lecture Notes in Computer Science",
  volume    = 4501,
  pages     = "340--354",
  year      = 2007
}