RankFinder
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"
,
Andreas Podelski
and
Andrey Rybalchenko
, in
VMCAI'2004
.
It main application is to prove disjunctive well-foundedness of
transition invariants
, and other relations. RankFinder is used in
Terminator
tool for termination proofs for systems code.
Download RankFinder for Linux/x86:
rankfinder
(
statically compiled
), and example input files
example1.pl
and
example2.pl
.
Back to homepage