Skip to content

Commit 0c8e723

Browse files
author
Matthieu Lemerre
committed
Upd
1 parent e58921b commit 0c8e723

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ store relations $$\pm x \pm y \leqslant c$$ for some constant $$c$$. These abstr
2424
polyhedra, but still expensive, in large part due to having to compute
2525
a transitive closure to find all known relations, which costs $$\mathcal O(|\mathbb X|^3)$$.
2626

27+
; Il manque des idées clés comme la constraint factorization pour supprimer des variables des domaines existants
28+
2729
Our goal is to find **a new family of relational abstract domains that are cheaper than the weakly-relational domains**.
2830
For this, a central question is **can we compute the expensive transitive closure much more cheaply?** The answer is yes, if we assume that the relation obtained on each path between
2931
two variables is always the same. This allows eliminating the vast majority of relations, **we only need to
@@ -35,7 +37,7 @@ style="width:700px; display:block; margin-left:auto; margin-right:auto">
3537

3638
<center>
3739
Fig. Graph of relations between variables. Each arrow represents a relation, labels have been omitted.
38-
Left is the initial configuration, middle is the computed closure, and right is a minimal spanning tree
40+
Left is the initial configuration, middle is the computed closure, and right is the minimal spanning tree that our domains only have to maintain.
3941
</center>
4042

4143
## Labeled union-find

0 commit comments

Comments
 (0)