Consider the following statement that appeared in Lee's Ranking functions for size-change termination (SCT).

Let $G$ satisfy the SCT condition.

There is an effective procedure to construct a $G$-ranking function expressed using only min, max and lexicographic tuples of program parameters and constants.

I'm interested mostly in the computational side of it. Has this been implemented before? If so, in which systems?

In fact, Lee's preliminary algorithm was made more practical by subsequent revisions in joint work with Ben-Amram and Codish. There remains the question of whether their claimed complexity is aceptable in current verifiers and whether it has already been tested in practice.


1 Answer 1


The complexity is acceptable in current verifiers, and has been implemented in at least the AProVE termination analysis tool for term rewrite systems.

They describe their implementation in Lazy Abstraction for Size-Change Termination, by Codish, Fuhs, Giesl & Schneider-Kamp, basing their implementation on the papers you refer to. Performance is good both from an expressiveness point of view and a run-time perspective.

The additional (clever!) trick is to pre-process the search for an appropriate abstraction and ranking function into a SAT problem (along with other search procedures for termination analysis) and having a SAT solver try to simultaneously find an instance. This trick is common in the termination analysis community.

  • $\begingroup$ I wonder if the same approach has been followed outside of term-rewrite based termination systems... $\endgroup$ Aug 17, 2018 at 8:52
  • 1
    $\begingroup$ @Rodrigo TRSes (augmented with primitive integers) are just a convenient notation for the termination behavior of a system. Often a step of abstraction is used to go from a more traditional programming language to a rewrite system. All the interesting program-language-specific tasks (pointer aliasing, etc) are done at this point. $\endgroup$
    – cody
    Aug 17, 2018 at 13:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.