Ranking function synthesis for bit-vector relations

• 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Nyckelord

Software verification

Ranking functions

Termination

Bit-vectors

Publikations- och innehållstyp

ref (ämneskategori)

art (ämneskategori)