Description
iRankFinder is an open-source termination analyzer for (integer) transition systems, namely control-flow graphs where edges are annotated with transition relations defined by linear constraints. It is written in Python (compatible with 2.7 and 3.X) and uses the Parma Polyhedra Library (PPL) and Z3 for manipulating (linear) constraints. It can be used via a web-interface or from a command-line.
The underlying techniques for proving termination are based on finding lexicographic- linear ranking functions, by incrementally ranking transitions (at the level of strongly connect components) using quasi-ranking functions. These are functions that are required to decrease for some transitions and not to increase for the rest.
Web Interface
iRankFinder is available online thanks to EasyInterface.
References
-
iRankFinder.
In 16th International Workshop on Termination, pages 83, 2018.
-
Control-flow refinement via partial evaluation.
In 16th International Workshop on Termination, pages 55, 2018.