<p>The complexity <em>is</em> acceptable in current verifiers, and has been implemented in at least the <a href="http://aprove.informatik.rwth-aachen.de/" rel="noreferrer">AProVE</a> termination analysis tool for term rewrite systems.</p>

<p>They describe their implementation in <a href="https://verify.rwth-aachen.de/fuhs/papers/LPAR10-scnp.pdf" rel="noreferrer">Lazy Abstraction for Size-Change Termination</a>, by Codish, Fuhs, Giesl &amp; 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.</p>

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

CC BY-SA 4.0
2018-08-17T08:52:12.973Z
I wonder if the same approach has been followed outside of term-rewrite based termination systems...
user1868607
CC BY-SA 4.0
2018-08-17T13:48:10.753Z
@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.
cody
CC BY-SA 4.0
2018-08-08T14:48:11.697Z
2018-08-08T14:48:11.697Z
cody
<p>Consider the following statement that appeared in <a href="http://www2.mta.ac.il/~amirben/downloadable/csl-ranking.pdf" rel="nofollow noreferrer">Lee's Ranking functions for size-change termination (SCT)</a>.</p>

<blockquote>
  <p>Let <span class="math-container">$G$</span> satisfy the SCT condition. </p>
  
  <p>There is an effective procedure to construct a <span class="math-container">$G$</span>-ranking function
  expressed using only min, max and lexicographic tuples of program
  parameters and constants.</p>
</blockquote>

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

<p>In fact, Lee's preliminary algorithm was made more practical by subsequent revisions in joint work <a href="https://arxiv.org/abs/0903.4382" rel="nofollow noreferrer">with Ben-Amram</a> and <a href="http://www2.mta.ac.il/~amirben/downloadable/tacas08.pdf" rel="nofollow noreferrer">Codish</a>. There remains the question of whether their claimed complexity is aceptable in current verifiers and whether it has already been tested in practice.  </p>

<program-verification><formal-methods>
Lee's algorithm for synthesis of ranking functions in size-change termination proofs
user1868607
# Lee's algorithm for synthesis of ranking functions in size-change termination proofs

(Asked by: username_0 on 2018-08-03)

Consider the following statement that appeared in [Lee's Ranking functions for size-change termination (SCT)](http://www2.mta.ac.il/~amirben/downloadable/csl-ranking.pdf).

> 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](https://arxiv.org/abs/0903.4382) and [Codish](http://www2.mta.ac.il/~amirben/downloadable/tacas08.pdf). There remains the question of whether their claimed complexity is aceptable in current verifiers and whether it has already been tested in practice.

**Tags:** program-verification, formal-methods

---

## 1 answers

### Answer by username_1 on 2018-08-08. Score: 6 | Accepted answer

The complexity *is* acceptable in current verifiers, and has been implemented in at least the [AProVE](http://aprove.informatik.rwth-aachen.de/) termination analysis tool for term rewrite systems.

They describe their implementation in [Lazy Abstraction for Size-Change Termination](https://verify.rwth-aachen.de/fuhs/papers/LPAR10-scnp.pdf), 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.

> **Comments:**
> **username_0**: I wonder if the same approach has been followed outside of term-rewrite based termination systems...  
> **username_1**: @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.  

---

