iRankFinder

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.

References

• iRankFinder. Doménech, Jesús J. and Genaim, Samir
  In 16th International Workshop on Termination, pages 83, 2018.
• Control-flow refinement via partial evaluation. Doménech, Jesús J., Genaim, Samir, and Gallagher, John P.
  In 16th International Workshop on Termination, pages 55, 2018.

Contributors