PV1 ⊧ iRankFinderinfers ranking functions for loops

Tool for inferring linear, lexicographic-linear and multiphase-linear ranking functions for multipath linear-constraint loops, with variables ranging over the rationals, reals, or integers.

Application domain/field

• Multiphase ranking functions
• Loop termination
• Ranking function

Type of tool

Termination analyzer? Ranking function finder?

Expected input

• Loop
• Choose algorithm that should be used to infer a ranking function

Format:

.mlc file (own syntax)

Expected output

Ranking function

Internals

This tool extends RankFinder by adding integers. Ranking function: a function $f$ that maps program states into elements of a well-founded ordered set, such that $f(s)>f(s^{\prime })$ holds whenever $s^{\prime }$ follows state $s$. This implies termination since infinite descent in a well-founded order is impossible.