Lasso Ranker

Ultimate LassoRanker is

• a tool for synthesizing termination and nontermination arguments for linear lasso programs via constraint solving,
• one toolchain of the Ultimate software analysis framework,
• a central component to Ultimate BuchiAutomizer,
• maintained by Matthias Heizmann and Jan Leike.

The class of programs that Ultimate LassoRanker operates on are called lasso programs. As the name indicates, the control flow graph of a lasso program is of a restricted shape: a stem followed by a loop. The figure below shows an example of a lasso program.

Ultimate LassoRanker can synthesize termination and nontermination arguments. Termination arguments generated consist of a ranking function and a set of linear inductive supporting invariants. For all states satisfying the invariants, the ranking function decreases after one loop execution. Different ranking functions can be synthesized on the basis on ranking templates. Currently affine-linear, nested, multiphase, lexicographic and piecewise ranking templates are implemented.

Ultimate LassoRanker is a central component of Ultimate BuchiAutomizer, which extracts lassos from larger programs and generalizes the synthesized termination arguments. Furthermore, Ultimate LassoRanker has been integrated into CPAchecker.

Publications

The theoretical foundations of Ultimate LassoRanker are described in the following publications.

• Jan Leike and Matthias Heizmann. Preprint of Geometric Nontermination Arguments. (2016)
• Jan Leike and Matthias Heizmann. Ranking Templates for Linear Loops. In LMCS 11(1) (2015).
• Jan Leike and Matthias Heizmann. Geometric Series as Nontermination Arguments for Linear Lasso Programs. International Workshop on Termination, 2014.
• Jan Leike and Matthias Heizmann. Ranking Templates for Linear Loops. In TACAS 2014.
• Matthias Heizmann, Jochen Hoenicke, Jan Leike and Andreas Podelski. Linear Ranking for Linear Lasso Programs. In ATVA 2013.

Web Interface

Ultimate LassoRanker is available via a web interface. This web interface allows `playing around' with lasso programs written C or the Boogie intermediate verification language.

Source Code

The source code of Ultimate LassoRanker is available on GitHub.

Current Restrictions

• For integer programs, computation of the integral hull of the loop transition is required. This is not yet implemented in our tool. Therefore the synthesis of affine-linear ranking functions over integer loops in incomplete.

SMT Solvers

Ultimate LassoRanker is built to interface with any SMT solver which implements the SMT-LIBv2 standard and is able to produce models of satisfiable formulas. Depending on the settings, our termination analysis uses the QF_NRA logic or the QF_LRA logic and our nontermination analysis uses the QF_NIA logic or the QF_LIA logic. Sample scripts are available in the SMT-LIB benchmark repository.