Change order

Author: Matthieu Lemerre

papers/2025-pldi-relational-abstractions-labeled-uf.md

@@ -76,6 +76,21 @@ However, labeled union-find cannot use relations like bounded
 difference $$a \le y - x \le b$$, as they are not injective. Doing so
 inevitably leads to precision loss.
 
+## Application
+
+Codex already performs [sophisticated constraint propagation](/papers/2024-pldi-compiling-with-abstract-interpretation.html)
+using relations between the values computed by the program. However, the new domain can find new relations, e.g. from relating simultaneously incremented loop counters:
+```c
+int i = 0, j = 4;
+while(i < 10) { i += 1; j += 3; }
+```
+Without labeled union-find, Codex learns that at the end of the loop, $$\mathtt{i} = 10$$,
+$$\mathtt{j} \in [4:+\infty]$$ and $$\mathtt{j} \equiv 1 \mathop{\mathtt{mod}} 3$$. However,
+with labeled union find and the TVPE relation, $$\mathtt{j} = 3\mathtt{i} + 4$$ is inferred.
+Thus, at the end of the loop, Codex knows $$\mathtt{j} = 34$$.
+
+The abstraction has also been implemented in the [Colibri2](https://colibri.frama-c.com/index.html) constraint solver to infer and propagate new relations efficiently.
+
 ## Combining with other abstractions
 
 Labeled union-find groups variables into related class, which each
@@ -103,21 +118,6 @@ Labeled union-find can also help relational abstraction similarly, shrinking the
 computation cost. Furthermore, it can be modified to detect any entailed equalities and notify other
 abstractions of these facts.
 
-## Application
-
-Codex already performs [sophisticated constraint propagation](/papers/2024-pldi-compiling-with-abstract-interpretation.html)
-using relations between the values computed by the program. However, the new domain can find new relations, e.g. from relating simultaneously incremented loop counters:
-```c
-int i = 0, j = 4;
-while(i < 10) { i += 1; j += 3; }
-```
-Without labeled union-find, Codex learns that at the end of the loop, $$\mathtt{i} = 10$$,
-$$\mathtt{j} \in [4:+\infty]$$ and $$\mathtt{j} \equiv 1 \mathop{\mathtt{mod}} 3$$. However,
-with labeled union find and the TVPE relation, $$\mathtt{j} = 3\mathtt{i} + 4$$ is inferred.
-Thus, at the end of the loop, Codex knows $$\mathtt{j} = 34$$.
-
-The abstraction has also been implemented in the [Colibri2](https://colibri.frama-c.com/index.html) constraint solver to infer and propagate new relations efficiently
-
 ## Going further
 
 - Read the [**paper**](/assets/publications/pdfs/2025-pldi-relational-abstractions-labeled-uf-with-appendices.pdf).