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.

BibTeX

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