cl-banner

Lazy Termination Analysis

Harald Zankl

PhD thesis, University of Innsbruck, 2009.

Abstract

“Lazy Termination Analysis” addresses various termination arguments and brings them to their full potential by encoding them as arithmetic constraints. Here lazy indicates that the actual work is done by somebody else, i.e., a SAT, PB, or SMT solver. Hence, unlike most contributions in this field, the thesis also goes beyond pure SAT solving by considering arithmetic constraints instead of plain propositional logic. How such constraints can be solved most efficiently by means of SAT, PB, or SMT techniques is also outlined.
One brilliant example demonstrating the benefits of our approach is the Knuth-Bendix order, which—-although already more than 40 years of age—-still lacks an efficient implementation. It turned out that the method can quite succinctly be encoded as linear arithmetic constraints which can then most efficiently be solved by current SMT solvers.
The expressiveness of SAT also allows to implement increasing interpretations, a variant of polynomial interpretations which at the same time also considers information from the dependency graph. As already suggested by its name this method allows some rules to temporarily increase the interpreted value.
This thesis also provides theory and empirical evaluation for matrices over the reals which makes it the first contribution that considers reals encoded in SAT.
That not only termination criteria are in the scope of arithmetic encodings is also demonstrated. To this end a looping reduction of given length involving only strings of given size is formulated as a satisfiability problem. Furthermore we formalized looping non-termination in the theorem prover Isabelle resulting in the first automated verifier capable of certifying non-termination.

Finally after all the (non-)termination encodings we investigate the other direction, i.e., encode propositional satisfiability as a termination problem in rewriting. Only the most simple formulas yield rewrite systems that can be handled by sophisticated termination analyzers. Hence this approach allows to easily generate testbeds of challenging rewrite systems. All encodings presented in this thesis have been integrated into the fully automatic (non-)termination analyzer TTT2.

 

  PDF

BibTeX 

@phdthesis{HZ09,
author = "Harald Zankl",
title = "Lazy Termination Analysis",
school = "University of Innsbruck",
year = 2009
}
Nach oben scrollen