cl-banner

SAT Solving for Termination Analysis with Polynomial Interpretations

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

Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lecture Notes in Computer Science 4501, pp. 340 – 254, 2007.

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.

 

  PDF |    doi:10.1007/978-3-540-72788-0_33  |  © Springer

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
}
Nach oben scrollen