RankFinder is a tool for the synthesis of linear ranking functions.
It implements the algorithm described in
"A complete method for the synthesis of linear ranking functions"
It main application is to prove disjunctive well-foundedness of
, and other relations. RankFinder is used in
tool for termination proofs for systems code.
Download RankFinder for Linux/x86:
), and example input files
Back to homepage