Ranking function synthesis is a key component of modern termination
provers for imperative programs. While it is well-known how to
generate linear ranking functions for relations over (mathematical)
integers or rationals, efficient synthesis of ranking functions for
machine-level integers (bit-vectors) is an open problem. This is
particularly relevant for the verification of low-level code. We
propose several novel algorithms to generate ranking functions for
relations over machine integers: a complete method based on a
reduction to Presburger arithmetic, and a template-matching approach
for predefined classes of ranking functions based on reduction to SAT-
and QBF-solving. The utility of our algorithms is demonstrated on
examples drawn from Windows device drivers.