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.
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.
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.
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.