# Mechanized Dominator Tree Certification

Jean-Christophe Léchenet

► To cite this version:

Jean-Christophe Léchenet. Mechanized Dominator Tree Certification. CPP 2026 - 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2026, Rennes, France. 10.1145/3779031.3779107. hal-05413838

HAL Id: hal-05413838

https://inria.hal.science/hal-05413838v1

Submitted on 12 Dec 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Mechanized Dominator Tree Certification

Jean-Christophe Léchenet

jean-christophe.lechenet@inria.fr

Université Côte d'Azur, Inria

Sophia Antipolis, France

## Abstract

In modern compilers, many optimizations and analyses, in particular those based on the SSA form, rely on dominance information, so computing dominators efficiently is an important problem. The classic algorithm to compute dominators in a control flow graph is the one designed by Lengauer and Tarjan in 1979. Other efficient algorithms have been proposed since. Previous works formally verified less efficient algorithms, and formally validated parts of the Lengauer-Tarjan algorithm, but there is no complete formal verification or validation of any of the fast algorithms computing dominators so far. In 2016, Georgiadis and Tarjan described a method to tackle these. They defined a certificate with which it becomes easy to validate dominators. Following their method, we successfully implemented and proved correct a validator of dominators in the Rocq Prover, inside the CompCertSSA verified compiler. This is the first complete mechanized certification of a fast algorithm computing dominators.

**CCS Concepts: Software and its engineering → Formal software verification; Compilers; Formal methods; Theory of computation → Graph algorithms analysis; Logic and verification; Program verification.**

**Keywords:** dominance, verified compilation, Rocq

## ACM Reference Format:

Jean-Christophe Léchenet. 2026. Mechanized Dominator Tree Certification. In *Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '26), January 12–13, 2026, Rennes, France*. ACM, New York, NY, USA, 14 pages. https://doi.org/10.1145/3779031.3779107

## 1 Introduction

Dominance information is an interesting property of a program characterizing how the flow goes inside the program. Given the Control Flow Graph (CFG) of a program with a distinguished entry node, we say that a node *u* of the graph dominates another node *v* if every path from the entry node to *v* goes through *u*. If, furthermore, *u* ≠ *v*, we say that *u* strictly dominates *v*.

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

CPP '26, Rennes, France

© 2026 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-2341-4/2026/01

https://doi.org/10.1145/3779031.3779107

Dominance analysis is one of the classic analyses performed by modern compilers [3]. It is needed for the construction of the popular SSA intermediate form [9], and plays a central role in it. The result of such an analysis can be stored efficiently in the form of the dominator tree, a tree in which a node is an ancestor of another one if and only if it dominates this other node. The parent of a node in the tree is the closest strict dominator of this node, dominated by all the strict dominators of this node, and is called the immediate dominator.

The classic algorithm computing dominators [18], due to Lengauer and Tarjan, dates back to 1979. It exists in two flavors: a simple version whose complexity is $O(m \log_{(m/n+1)} n)$ (where *n* is the number of vertices and *m* the number of arcs of the CFG) and a more complex version that achieves $O(m\alpha(m, n))$ where $\alpha$ is a functional inverse of the Ackermann function. Several variations and alternatives (e.g. [6, 10], see [12] for a survey) have been proposed since, but the Lengauer-Tarjan algorithm remains the standard one.

The question of formally proving an algorithm that builds the dominator tree, interesting in itself, gained interest with the arising of formally verified compilers, such as CompCert [19, 20]. In the context of a formally verified compiler, if a transformation critically relies on some dominance information, it is not only desirable, but required, to prove at least some properties about the dominator tree. Note however that it is not necessary to prove all the properties of the dominator tree to make some interesting use of it, as done e.g. in [5] described below.

Two previous works tackle the problem of formally verifying algorithms computing dominators.

In the context of Vellvm [22], a formal framework in Rocq for reasoning about the semantics of LLVM IR and formalizing transformations operating on LLVM IR, Zhao and Zdancewic [23] give a specification of computing dominators, and instantiate it on two iterative algorithms, the one (AC) from Allen and Cocke [1] and the optimized one (CHK) from Cooper et al. [7]. They prove that both algorithms are both sound and complete, meaning that what they compute is exactly the dominance relation. They also prove a construction of the dominator tree. The limitation of this work is that both AC and CHK have complexity $O(mn^2)$. Although CHK is reported to perform well in practice on graphs of reasonable size, it is outperformed by Lengauer-Tarjan on large graphs [12].

In the context of CompCertSSA [4], a fork of CompCert with an SSA middle-end, Blazy et al. [5] show the correctness
<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /><figcaption>**Figure 1.** A CFG and the associated dominator tree</figcaption></figure>

CFG, node *c* dominates node *d*, since all the paths from the entry, node *a*, to node *d*, go through node *c*. Thus node *c* is an ancestor of node *d* in the dominator tree. Node *d* has 3 dominators: nodes *a*, *b*, and *c*. Nodes *a* and *b* dominate node *c*, thus *c* is the immediate dominator of node *d*, and thus its parent in the dominator tree. On the contrary, node *c* does not dominate node *e*. To prove that, it is sufficient to exhibit a path from node *a* to node *e* that does not go through node *c*: *a*-*b*-*h*-*g*-*e*. Thus node *c* is not an ancestor of node *e* in the dominator tree. Node *e* does not dominate node *c* either (path *a*-*b*-*c*), thus nodes *c* and *e* are unrelated in the tree.

We add two hypotheses on entry and cfg guaranteeing
the well-formedness of the CFG.

Hypothesis entry_no_pred : $\forall$all i, $\neg$ cfg i entry.
Hypothesis cfg_reached :
forall i j, cfg i j $\rightarrow$ reached i.

entry_no_pred ensures that entry has no incoming arc in
the graph. cfg_reached ensures that every node in the graph
is reachable from entry. These two hypotheses help reason
in Rocq like we do on paper: the statements and the proofs
are more natural, at the cost of two hypotheses to prove
when calling the lemmas. [5] made another choice. They do
not have these axioms in their formalization, but have to deal
with cases we do not consider on paper. For instance, some
of their lemmas assume that a given node is reachable from
entry, which does not appear on paper, since the assumption
that all nodes are reachable from the entry node is implicit.<fnref n="1" />

These are the only hypotheses made on the CFG. Apart
from satisfying these two conditions, the CFG can be ar-
bitrary. In particular, it may contain cycles and be non-
reducible.

2.2 Candidate Tree

The candidate dominator tree is formalized as a function T associating to each node its parent in the tree, and None to the root of the tree, since it has no parent.

Variable T : node $\rightarrow$ option node.

Definition has_parent u v := T u = Some v.

Definition Tstar := clos_refl_trans _ has_parent.

Variable root : node.

Hypothesis T_root : T root = None.

Hypothesis T_tree :
forall u, T u $<>$ None $\rightarrow$ Tstar u root.

has_parent u v holds when v is the parent of v in T. Tstar
is the reflexive and transitive closure of has_parent, it is thus
the ancestor relation: Tstar u v means that v is an ancestor
of u in T. T_root and T_tree specify that T is a tree rooted at
root: root has no parent, and is an ancestor of every other
node in the tree.

Here again, we made some different choices from those [5]
did. In [5], the candidate tree has type node $\rightarrow$ node and
satisfies T root = root, meaning that root has a parent, itself.
Actually, we made initially the same choice, but changed to
a formalization closer to paper reasoning when the proofs
became complex and it became hard to transpose the paper
proofs in Rocq.

In the same spirit of making our formalization more natu-
ral, we add the following two hypotheses ensuring that the
nodes in the tree are nodes of the graph.

Hypothesis T_root_reached : reached root.
Hypothesis T_reached :
forall u, T u $<>$ None $\rightarrow$ reached u.

T_root_reached assumes that root is reachable from entry
in the CFG. T_reached assumes the same for all nodes that

<footnote n="1">¹To be fair, in our formalization, a node can exist but have no incoming or
outgoing arc in the graph, which is also a case we do not consider on paper.
In this regard, the two hypotheses we use are not enough to make reasoning
in Rocq just like reasoning on paper, but it makes the two situations closer.</footnote>
have a parent in T. Since T is a tree, all nodes are covered
by these two hypotheses. Once again, these hypotheses are
completely natural (we do not want to manipulate a graph
and a tree that have nothing to do with each other), but we
have to write them down, and we will have to prove them
when calling the lemmas depending on them.

## 2.3 The Parent and Sibling Properties

Georgiadis and Tarjan define two properties on trees that, combined, are equivalent to being the dominator tree.

The first one, called the parent property and Tici parent in
the formalization, specifies that the parent of a node (in T)
is an ancestor of any predecessor of that node in the graph.
This captures the fact that the immediate dominator of a
node dominates any predecessor of that node.

Definition T\_parent := $\forall$all i j, cfg i j $\rightarrow$
exists k, T j = Some k $\wedge$ Tstar i k.

Let us illustrate this definition on the tree of Figure 1b,
that satisfies the parent property. The parent of node e is
node b. It has two predecessors, node d and node g, and node
b is indeed an ancestor of both.

We can prove several interesting lemmas about T\_parent.
The main one is the soundness of T [14, Corollary 2.3]: if v is
an ancestor of w in T, then v dominates w.

Corollary corollary_2_3 : Tici parent $\rightarrow$
forall v w, Tstar w v $\rightarrow$ dom v w.

Actually, the same property is used in [5] (they call it
D\_cfg): it is the key property they check to ensure that the
dominance test they build from the tree is sound.

T\_parent has other corollaries, maybe unexpected, about
the tree structure of T.

Lemma T\_parent_root_entry : T\_parent $\rightarrow$
root = entry.

Lemma T\_parent_spreading : T\_parent $\rightarrow$
forall u, u $<>$ entry $\rightarrow$ reached u $\rightarrow$ T u $<>$ None.

Lemma T\_parent_reached_in_tree : T\_parent $\rightarrow$
forall u, reached u $\rightarrow$ Tstar u entry.

T\_parent_root_entry shows that the root of the tree is
necessarily entry. This means that we do not need to check
that fact if we already check T\_parent (in [5], this distinction
between root and entry is not made, there is only entry).
T\_parent_spreading shows that T is spanning: each reachable
node that is not entry has a parent in T. The last corollary,
T\_parent_reached_in_tree, is probably the most surprising:
every reachable node has entry as an ancestor in T, which
means that T is a tree! What makes this lemma interesting is
that it does not make use of hypothesis T\_tree: it is enough
to check T\_parent to ensure that T is a tree.<fnref n="2" /> This is used in
practice in the formalization (see Section 3.2).

Property T\_parent specifies half of what we expect of
the dominator tree: soundness. What about completeness?
Clearly, T\_parent is not sufficient for completeness. The flat
tree, for instance, where every node other than entry has
entry as its parent, trivially satisfies T\_parent. But in general,
this is not the dominator tree! So we need a second property
on T for it to be the dominator tree.

This second property is called the sibling property in [14]
and T\_sibling in the formalization. It states that two siblings
in the tree do not dominate each other. Intuitively, it rules
out any candidate tree that would be too flat, and the flat
tree in particular. If a node is dominated by another one, it
cannot be at the same level in the tree as this other node, it
has to be below it in the tree.

Definition T\_sibling :=
forall v w, v $<>$ w $\rightarrow$ T v = T w $\rightarrow$ not dom v w.

The tree of Figure 1b satisfies also the sibling property.
Nodes *h* and *g* have the same parent, node *b*. And, indeed,
they do not dominate each other: *a*-b-*h* shows that node *g*
does not dominate node *h*, and *a*-b-*c*-g that node *h* does not
dominate node *g*. On the contrary, node *c* dominates node *d*,
therefore nodes *c* and *d* cannot be siblings. And indeed, they
are not, node *c* is the parent of node *d*.

It is not surprising that the dominator tree of Figure 1b satisfies the parent and sibling properties, since it is the case of any dominator tree. The converse is true too. Combined with T\_parent, T\_sibling is equivalent to T being the dominator tree [14, Theorem 2.5].

Definition T\_is\_dom :=
forall u v, Tstar u v $\leftrightarrow$ dom v u.

Theorem theorem_2_5 :
T\_parent $\wedge$ T\_sibling $\leftrightarrow$ T\_is\_dom.

T\_parent is easy to check directly, but not T\_sibling. We
need an intermediate object to ease the verification. This is
where the notion of low-high order comes into play.

## 2.4 Low-High Orders

A low-high order is in particular a preorder on tree T, so we
start by assuming a preorder pre on T (note that this is a
preorder on the tree, not on the CFG).

Variable pre : node $\rightarrow$ Z.
Hypothesis pre_inj : $\forall$u v,
reached u $\rightarrow$ reached v $\rightarrow$ pre u = pre v $\rightarrow$ u = v.

Hypothesis preVOlt : $\forall$u u',
T u = Some u' $\rightarrow$ pre u' < pre u.

Hypothesis pre_consecutive : $\forall$v x y,
reached x $\rightarrow$ reached y $\rightarrow$
Tstar x v $\rightarrow \neg$ Tstar y v $\rightarrow$
pre y < pre v $\lor$ pre x < pre y.

pre associates to each node a relative integer, unique per
pre_inj. It is assumed to be a preorder using a classic axiom-
atization: the parent of a node has a smaller number than

<footnote n="2">²This is an exception, all the lemmas make an heavy use of the hypotheses.</footnote>
<figure><img src="image_5.png" /><figcaption>**Figure 2.** The divergent spanning trees *B* and *R* built from the CFG and the low-high order of Figure 1</figcaption></figure>

this node (`preparelt`), and a node `y` that is not in the subtree of a node `v` either has a number smaller than `v` (if it was visited before `v`) or (if it was visited after `v`) a number greater than every descendant `x` of `v` (`pre_consecutive`). We can observe that this time we did not escape the hypotheses about reached. This is because `pre` is assumed to be a total function over type node, so we must restrict our hypotheses to the nodes in the graph. We could have made another choice, for instance to use type option like we did in the type of $\Gamma$, but we would have had to wrap and unwrap `pre` each time we refer to it, which would have been equally cumbersome. This is a trade-off, this time we chose to have a total function and to add hypotheses about reached.

This preorder `pre` is a numbering on the tree. Property low-high relates it to the graph. A preorder is low-high on the graph if for every node `v` that is not entry, either there is an arc in the CFG between its parent in $\Gamma$ and `v`, or there are two arcs (`u`, `v`) and (`w`, `v`) such that `u < v < w` in this preorder and `w` is not a descendant of `v` in $\Gamma$. The direct translation of this in Rocq is the following.

Definition low_high_order := **forall** v,
  reached v → v < > entry →
  (exists u, T v = **Some** u ∧ **cfg** u v)
  ∨ exists u w,
    cfg u v ∧ **cfg** w v
    ∧ pre u < pre v < pre w ∧ ¬ Tstar w v.

But given that the graph and the tree have the same nodes, we use a different, equivalent but more convenient definition in the formalization.

Definition low_high_order := **forall** v v',
  T v = **Some** v' →
  cfg v' v
  ∨ exists u w,
    cfg u v ∧ **cfg** w v
    ∧ pre u < pre v < pre w ∧ ¬ Tstar w v.

Let us illustrate this concept of low-high order. The tree in Figure 1b is labeled with a low-high order on the CFG. The entry node (a) and nodes that have only one predecessor (b, c, d, h) impose no direct constraint on the labeling. Indeed, for the latter, their predecessor in the CFG is their parent in $\Gamma$, so we fall in the first case of the low-high order definition. There is still a constraint, though: a low-high order is a preorder, so for instance d must have a label greater than the label of c. But the nodes with two predecessors (e, f, g) are more interesting, since they exercise the second case of the low-high order definition. For instance, the label of f (5) is between the label of h (3) and the label of e (6), and e is not a descendant of f in the tree.

## 2.5 Divergent Spanning Trees

We need to prove a link between properties $\Gamma$_sibling and low_high_order. The proof proposed in [14] involves defining two auxiliary spanning trees *B* and *R* rooted at entry from the low-high order. They describe an algorithm ([14, Algorithm 1]) constructing these trees. We preferred the simplified version ([13, Algorithm 1']) that they describe in an addendum. This simplified version has the additional advantage that it matches exactly the low-high order definition. For each node distinct from entry, the algorithm describes two disjoint cases to build an arc for *B* and an arc for *R*, corresponding to the two cases of the low-high order definition. Intuitively, given a node `v` distinct from entry, if there is an arc between its parent in $\Gamma$ and `v`, then add this arc to both *B* and *R*; if not, and if there are two arcs (`u`, `v`) and (`w`, `v`) such that `u < v < w` in low-high order and `w` is not a descendant of `v` in $\Gamma$, then add (`u`, `v`) to *B* and (`w`, `v`) to *R*.

We illustrate *B* and *R* on the CFG and the low-high order of Figure 1. They are shown in Figure 2, labeled with the low-high order. For nodes *b*, *c*, *d* and *h*, their parent in $\Gamma$ is one of their predecessors in the CFG (the only one, actually), therefore it is also their parent in both *B* and *R*. For *e*, *f* and
<figure><img src="image_6.png" /><figcaption>Figure 3. Definitions of B and R</figcaption></figure>

g, that each have two predecessors in the CFG, the one with a smaller label is their parent in B, the other one is their parent in R. For instance, the predecessor of f (with label 5) with a smaller label is h (with label 3), thus arc (h, f) is in B. The other predecessor is e (with label 6), thus arc (e, f) is in R.

Since we work with an abstract specification, and since in
our case B and R are just proof artifacts, we specify rather
than construct the trees. And we add extra conditions to
make sure this defines uniquely the two trees.

Definitions of B and R are shown in Figure 3. For a node
v, if the parent v' in T is a predecessor of v, then v' is the
parent of v in B and R (constructors B1 and R1). Otherwise
(con构造ers B2 and R2), if v has two predecessors u and w
with pre u < pre v < pre w and w not a descendant of v in
T, then u is the parent of v in B, and w is the parent of v in
R. The last conditions in B2 and R2 are not in [13]. They are
for cases where several predecessors satisfy all the other
conditions. There is no example in Figure 1, since this arises
only on nodes with at least 3 predecessors. In that case,
any matching predecessor work, but we specify the one we
select: the predecessor with the greatest label in B2 and the
predecessor with the smallest label in R2.

We now prove that the specifications really define two
spanning trees with some interesting properties. We assume
first a few natural but technical assumptions: the numbering
is upper-bounded (pre_bounded), and for each node u we can
compute pred u, the list of its predecessors (preds correct).
These hypotheses are needed for the proofs.

Hypothesis pre_bounded :
  exists M, `forall u, pre u <= M.`

Variable preds : node → list node.
Hypothesis preds correct :
 forall u v, In u (preds v) ↔ cfg u v.

And we assume that T satisfies the parent property and
pre is a low-high order.

Hypothesis parent : Tellan.
Hypothesis pre_low_high : low_high_order.

We start by proving that B and R are properly defined.

Lemma B_exists : `forall v,
v <> entry → reached v →
exists w, B v w.`

Lemma B_function : `forall v, uniqueness (B v)`.

Lemma B_exists shows that any vertex v distinct from
entry has a parent in B. This is trivial since pre is a low-high
order. Lemma B_function shows that this parent is unique.
The same lemmas can be proved on R.

Then we prove two properties, one for B and one for R,
that are the main ingredients to prove theorem theorem_2_10
below.

Lemma B_pre : `forall u v, B u v → pre v < pre u.`
Lemma lemma_2_7 : `forall v v', T v = Some v' →
clos_refl_trans _
  (fun x y ⇒ pre v <= pre x ∧ R x y) v v'.`

Lemma B_pre states that, in tree B, a parent has a smaller
number than its children. This directly follows from the
definition of B, and can be checked on the tree of Figure 2a.
Lemma lemma_2_7 (translated from [14, Lemma 2.7]) is more
complex. Intuitively, it means that, given a node v and its
parent v' in T, there exists a path in R from v' to v, and all
<table><caption>**Table 1.** Number of lines of code of each part of the certifier (New) and of the previous implementation (Old), with the percentage of code reused in New from Old.</caption><thead><tr><th>Part</th><th>Old</th><th>New</th><th>Code reused</th></tr></thead><tbody><tr><td>Dominance theory (Rocq)</td><td>430</td><td>2070</td><td>21%</td></tr><tr><td>Candidate tree (OCaml)</td><td>200</td><td>500</td><td>40%</td></tr><tr><td>Building objects (Rocq)</td><td>1080</td><td>2420</td><td>45%</td></tr><tr><td>Tree validation (Rocq)</td><td>60</td><td>680</td><td>9%</td></tr><tr><td>Interface (Rocq)</td><td>30</td><td>280</td><td>11%</td></tr></tbody></table>

sorted to be accepted by the checker, meaning that each parent of an arc must appear as the child of another arc before, except the entry node. This is easily achieved by having a preorder on the candidate tree and sorting the arcs with respect to the number of the child, putting the smallest number first. We reuse the exact same interface, but using the candidate low-high order as the preorder. This means, in particular, that the result returned by the updated OCaml code constructing the candidate tree is still accepted by the old Rocq checker, which conveniently allowed us to do the update in two steps.

We also reuse from [5] the architecture of the Rocq part: taking the list of arcs as inputs, it first constructs three intermediate objects: a map associating to a node its candidate immediate dominator, the candidate dominator tree, and a labeling of this dominator tree. Then, using these three objects, it performs efficiently the check of property $T_{parent}$.

Compared to the implementation of [5], we make the following changes. We augment the unverified OCaml implementation with the computation of a low-high order (Section 3.1). We strengthen the properties proved on the three intermediate objects (Section 3.2). The code constructing these objects is mostly reused, but new proofs are added, in particular regarding completeness. We update the main check so that it verifies that the order is low-high in addition to proving property $T_{parent}$ (Section 3.3). We expose to the rest of the compiler a new interface with more functions and stronger properties (Section 3.4).

To give an idea of the size of each part of the implementation, we show in Table 1 the number of lines of code of each part, comparing the old implementation and ours, emphasizing the proportion of code that we reused from the previous checker. The table also has a line for dominance theory. This includes some basic definitions and properties related to dominance that are already present in CompCertSSA, in addition to the theory described in Section 2 in the case of the new implementation.

## 3.1 Construction of the Candidate Tree and Order

In [14], Georgiadis and Tarjan describe three ways of computing a low-high order. Since the code in CompCertSSA

builds the dominator tree from the semidominators following the Lengauer-Tarjan algorithm [18], it was natural to use the version relying on semidominators [14, Section 6].

Based on the existing OCaml implementation of the simple version of the Lengauer-Tarjan algorithm, we implemented several optimizations described in [15], added some instrumentation and returned objects that were already computed but not returned. Compared to the previous implementation, we return: parent, an encoding of a depth-first spanning tree; semi, the semidominators; rd, the relative dominators; and g, where $g(v)$ is the last node on some semidominator path from semi($v$) to $v$ (see [14] for precise definitions).

From that, we implemented [14, Algorithm 8] that builds two divergent spanning trees $B$ and $R$. Based on these trees, we can compute a low-high order with an implementation of [14, Algorithm 7], relying also on Algorithms 3 and 5 from the same paper and some ideas described in [11].

Georgiadis and Tarjan mention a simpler alternative to Algorithm 7, that they conjecture correct. They could not prove it, but tested it experimentally with other authors without finding any counter-example [11]. This alternative is described in slightly different versions in [14] and [11]. We implemented the one described in [11] that has the advantage of building a connected graph, that is easier to visit.

We have thus two implementations building a low-high order. This illustrates the strength of the certified approach. We are free to edit the unverified OCaml code, and this is easy, since there is no proof about it. And since we run a verified checker afterwards, we cannot go silently wrong. At worst, compilation fails because the checker was not able to verify the candidate tree.

The low-high order is used to sort the list of arcs that is then sent to the Rocq verifier.

Changing the original code to make it compute a low-high order was not difficult. Indeed, the only deep change to existing code is the instrumentation mentioned above and it is light. The rest of the changes are code additions, disjoint from the existing code. What turned out to be more difficult was to implement the new algorithms as efficiently as they should be. Although the algorithms are well described in the papers, it was hard to get every detail right at first, in particular regarding the choice of data structures, and our first implementations in OCaml performed poorly. There is certainly still room for improving performance in the current implementation.

## 3.2 Constructing Intermediate Objects

In Rocq, the OCaml code is abstracted as a function `extern_d`.

Axiom `extern_d`: node → code → list (node * node).

`extern_d` entry f returns the candidate dominator tree of the CFG of function f with entry entry, encoded as mentioned above as a list of arcs (child, parent).
We reuse from [5] the code constructing, from the list of arcs, a map associating to a node its candidate immediate dominator, the candidate dominator tree, and a labeling of this dominator tree based on depth-first search enabling fast ancestor checking. Only the construction of the candidate dominator tree was slightly changed. We reuse also the proofs made about these objects (some proofs related to the labeling are also taken from [17]), and add new ones, in particular regarding completeness. We describe each of the three objects below, emphasizing differences with [5].

**Building a fast access to the candidate immediate dominator.** From the list of arcs, we can build a better data structure, namely a finite map, to have a fast access to the parent of each node, i.e. to the immediate dominator of each node. This is the role of function `make_D fun`.

Definition make_D fun (l : list (node * node))
: node → option node.

It is designed to be applied partially. If l is the list of arcs, `make_D fun` builds internally a map associating to a node its parent, and wraps it in a function of type node → option node implementing the parent function T of Section 2.2. Function `make_D fun` is reused from [5], except that it now returns an option type, to match the difference in the modeling of T mentioned in Section 2.2.

**Building the candidate dominator tree.** From the list of arcs, the checker also builds the tree whose arcs are those of the list, i.e. the candidate dominator tree. The starting point is an empty tree, and the arcs are added one by one to the tree in the order of the list. Each time an arc (child, parent) is added, it is checked that it does not introduce a cycle by verifying that the parent has already been seen, while, on the contrary, the child has not been seen yet. This, in particular, checks that child and parent are two distinct nodes, and that (child, parent) is not a self-loop. This procedure only works if the arcs are processed in the right order, that's why it is required from the OCaml code to return a topologically sorted list of arcs.

Building the tree is done by function `build` reused from [5], with one significant difference. In [5], the check that there is no cycle is implemented thanks to a set seen of processed nodes, initialized to the singleton `{entry}`, and growing when processing a new arc. This implementation ensures that the constructed object is connected, and thus that it is indeed a tree. On the contrary, in our implementation, the check is implemented as a set `not_seen` of unprocessed nodes, initialized to the set of nodes in the CFG minus node entry, and decreasing when processing a new arc. Precisely, when a new arc (child, parent) is processed, we check that child is in `not_seen` and parent is not. This gives for free that the nodes of the constructed object are also nodes of the CFG (needed to instantiate hypothesis `T_reached`), but, unlike the

previous check, this does not ensure that the object is connected. This means that the object may not be a tree but a forest. This is where lemma `T_parent_reached_in_tree` (see Section 2.3) comes into play. Since we will check that the object satisfies `T_parent`, lemma `T_parent_reached_in_tree` guarantees that this is indeed a tree.

Function `buildapi` has the following type.

Definition buildapi {A:Type} (entry:node)
  (l : list (node*node)) (not_seen : tree A)
  : option (tree (list node)).

Type tree A is a type of finite maps with keys of type node and values of type A. Eventually, it is instantiated as `Ptree.t A`, a type of binary tries inherited from CompCert, where keys are of type positive, the standard type of positive binary numbers.<fnref n="3" /> The type of `not_seen` is polymorphic, because it is actually used as a set of keys, so the type of the values does not matter. Defining it polymorphically allows to pass the CFG as `not_seen` without any transformation. The function returns a tree of type tree (list node) (the value attached to a node is the list of its children) if it succeeds, and `None` if it fails.

We can prove a few basic properties about `buildapi`, when it succeeds, that are direct consequences on the tests made with `not_seen`. Here is one important property.

Theorem buildapi_no_repet : $\forall$ l not_seen sn,
buildapi entry l not_seen = Some sn $\rightarrow$
NoRepetTreeN (sons sn) entry (S fuel).

Theorem buildapi_no_repet (already in [5]) specifies that the generated object `sn` is well-formed. Function `sons` is a wrapper to see `sn` as a function `node → list node` associating to each node the list of its successors in `sn`. Predicate `NoRepetTreeN` means that, starting from entry, accessing recursively the successors in `sn` lead to pairwise distinct nodes, and thus `sn` is a tree rooted at entry. Actually, since `sn` may not be connected, precisely this means that the connected component of `sn` which contains entry is a tree rooted at entry. Predicate `NoRepetTreeN` is indexed by a natural number `fuel` that is the maximal depth considered. This is inherited from [5]; please refer to it for an explanation.

We can prove a link between `buildapi` and `make_D fun`.

Lemma in_sons_D : $\forall$ entry l not_seen sn,
buildapi entry l not_seen = Some sn $\rightarrow$
forall i j,
In j (sons sn i) $\rightarrow$ make_D fun l j = Some i.

Lemma D_in_sons : $\forall$ entry l not_seen sn,
buildapi entry l not_seen = Some sn $\rightarrow$
forall i j,
make_D fun l i = Some j $\rightarrow$ In i (sons sn j).

<footnote n="3">³From version 3.10, CompCert uses a smarter type [2], but we are based on version 3.9 of CompCert, before the change.</footnote>
Lemma in_sons_D, already in [5], shows that if j is a child
of i in sn returned by build, then i is its parent ac-
cording to make_D Fun 1. Lemma D_in_sons, new since it was
not needed for soundness, only for completeness, shows the
converse.

Combining both and by a simple induction, we can prove
the following lemma.

Lemma Tstar_InSubTree_iff : `forall entry l not_seen sn,
build entry l not_seen = Some sn ->
forall i j,
Tstar (make_D fun 1) i j ↔ InSubTree (sons sn) j i.`

Intuitively, lemma Tstar_InSubTree_iff states that j is
an ancestor of i in the tree encoded by make_D fun 1 if and
only if i is a descendant of j in sn (InSubTree (sons sn) is
intuitively the reflexive and transitive closure of sons sn). In
other words, they are two encodings of the same tree.

**Numbering the nodes.** On the result of `buildapi`, a classic left-to-right depth-first search is performed on the tree and each node is given a pair of numbers: the first one the first time it is visited and the second one the last time it is visited. This numbering is used twice.

First, if we consider only the first components of the pairs,
we get a preorder. It is used as the low-high order. This is
where the order of the list of arcs returned by OCaml is
important. It decides the order in which the nodes are visited
during the traversal and thus the way they are numbered.

Second, each pair can be seen as an interval, as in [5].
When we want to compare two nodes from the trees, we can
compare the associated intervals, and deduce if one of the
node is an ancestor of the other (if there is an inclusion), or
if one is on the left of the other. This is a standard property
of a numbering induced by a depth-first search traversal [8].
We refer the reader to [5] for an illustration of intervals. [14]
recommends something a bit different, annotating each node
with a preorder number and the size of the subtree rooted at
this node, but this has the same properties.

The implementation `build_itt_map` is reused from [5].

Definition build_itt_map
    (entry: node) (sn: tree (list node))
    : option (tree itv).

It takes as inputs the entry node and the tree `sn` built by
`buildapi` and returns a finite map where each node is
associated to an interval of type `itv`, a pair of two numbers.
The exact implementation of `itv` is discussed below.

We can prove about `build_itt_map` two main lemmas,
soundness and completeness.

Lemma build_itt_map: `forall entry sn itvm,
build_itt_map entry sn = Some itvm ->
forall n1 n2 itv1 itv2,
get n1 itvm = Some itv1 ->
get n2 itvm = Some itv2 ->
itv_Incl itv1 itv2 -> InSubTree (sons sn) n2 n1.`

Lemma build_itt_map_complete: `forall entry sn itvm,
NoRepetTreeN (sons sn) entry (S fuel) ->
build_itt_map entry sn = Some itvm ->
forall n1 n2 itv1 itv2,
get n1 itvm = Some itv1 ->
get n2 itvm = Some itv2 ->
InSubTree (sons sn) n2 n1 -> itv_Incl itv1 itv2.`

Lemma build_itt_map_sounds establishes that if we have
two nodes n1 and n2, and the interval `itv1` associated to
n1 is included in the interval `itv2` associated to n2, then
n1 is a descendant of n2 in sn. (get is a lookup function in
objects of type tree A.) This lemma comes from [5], but in-
terestingly, the former statement contained an hypothesis
NoRepetTreeN (sons sn) entry (S fuel) that is actually not
needed (this was first observed in [17]). The other lemma,
build_itt_map_complete (new), is the converse. If n1 is a de-
scendant of n2, then we have the inclusion of the correspond-
ing intervals. Note that this time, we do have the hypothesis
about NoRepetTreeN.

Inherited from [5], the integers used in type `itv` are ab-
stracted behind an interface (a *Module Type* in Rocq).

Module Type INT.
Parameter t : Type.
Parameter int_zero : t.
Parameter intapi : t -> option t.
...
End INT.

Module Make (I:INT).
...
Record itv := { pre: I.t; post: I.t }.
...
End Make.

The type of integers used (I.t) is opaque, we only ex-
port some operations on it. We have access to number 0
(int_zero), a successor operation (intapi) that may fail if
the integer type is finite, a comparison function and proper-
ties about these objects that we omit.

Abstracting the type of integers allows to switch between
several implementations: in particular, the standard relative
binary numbers Z or the efficient primitive integers Int63
that Rocq features.<fnref n="4" /> In [5], this works well because what is
exported is an ancestor test of type node → node → bool, so
the type of integers does not leak. In our implementation,
however, we need more. We need a way to compare the pre-
order numbers of nodes to check that the order is low-high,
with the additional difficulty that property low_high_order
(this is also the case of hypothesis pre_bounded) is about a
preorder of type Z, so we need to relate I.t and Z.

<footnote n="4">⁴These are unsigned integers, named Int63 in the version of Rocq we use (8.13). In version 8.14 of Rocq, they were renamed into `uint63` to better reflect that they are unsigned integers.</footnote>
Our solution to this is twofold. First, instead of exporting
the raw preorder, we define a comparison function `itv_cmp`
that compares two intervals.

Variant `itv_comparison` :=
| Smaller | Greater | Included | Includes.

Definition `itv_cmp` (`it1` `it2` : `itv`) : `itv_comparison`.

`itv_cmp` `it1` `it2` can have four different values: Smaller if `it1` is smaller than `it2` (meaning `it1`.(`post`) < `it2`.(`pre`)), Greater if `it2` is smaller than `it1`, Included if `it1` is included in `it2`, and Includes if `it2` is strictly included in `it1`.

From that, we can define easily a comparison function
on nodes (`node_cmp`) with default values if at least one node
has no associated interval. Function `is_ancestor` that checks
ancestor relationship is just a specialization of it.

Definition `node_cmp` (`itvm`: tree `itv`) (`n1` `n2`: `node`) :=
match `get n1` `itvm`, `get n2` `itvm` with
| `None`, `None` ⇒ `Included`
| `None`, `_` ⇒ `Smaller`
| `_`, `None` ⇒ `Greater`
| `Some` `itv1`, `Some` `itv2` ⇒ `itv_cmp` `itv1` `itv2`
end.

Definition `is_ancestor` `itvm` (`n1` `n2` : `node`) :=
match `node_cmp` `itvm` `n2` `n1` with
| `Included` ⇒ `true`
| `_` ⇒ `false`
end.

These functions do not expose type `I.t` anymore, only
`itv_comparison` and `bool`.

Second, we note that each integer occurring in the labeling
is computed as `int` iterated a finite number of times on
`int_zero`. We can prove it for the pre component (the same
lemma is proved for post).

Lemma `build_itv_map_pre_int` : `forall` `sn` `itvm`,
`build_itv_map` `sn` = `Some` `itvm` →
`forall` `n` `itv`, `get n` `itvm` = `Some` `itv` →
{ `i` | `iter` `int` `i` `int_zero` = `Some` `itv`.(`pre`) }.

For any interval `itv` associated to a node `n`, there exists
an integer `i` such that `itv`.(`pre`) is `int` iterated `i` times
on `int_zero`. Notation `{ `i` | ... }` is an existential quantifi-
cation in universe `Type`, while standard existential quantifi-
cation is in the universe `Prop` of propositions. We use the
version in `Type`, because, unlike the version in `Prop`, we can
extract the corresponding integer. This integer can be seen
as a number in `Z`, and we can show that it behaves the same
as the integer in `I.t` from which it was extracted (in partic-
ular, comparing them with the corresponding operators is
equivalent).

Doing that for every node, we get a numbering of each
node with pairs of integers in Z, equivalent to the numbering
in I.t, that we can use in the proofs, in particular to rea-
son about `low_high_order`. We prove a counterpart to each

lemma about `build_itv_map` that uses the numbering in Z
instead. We also prove a correctness lemma for `node_cmp`
also using the numbering in Z.

## 3.3 Validating the Tree

Using the fast access to the parent and the numbering, the
checker validates that the candidate tree has the right prop-
erties. In [5], they verify that the tree has property `Tparent` in a traversal of the CFG. In our work, we verify both that
it has property `T parent` and that the order is low-high, in a
single traversal of the reversed CFG (property low-high is
easier to check on the reversed CFG, and checking `T parent` is as easy as on the CFG).

Property `TVOparent` is checked according to its definition,
using the fast access to the parent and the intervals for fast
ancestor checking. For checking property low-high, we also
use the intervals, by making the following observations. Let
us consider a node `v` and one of its predecessors `v'`. If `v`'
is the parent of `v` in `T`, the first case of the low-high order
definition applies. Otherwise, we consider the four possible
values for the result of `node_cmp` `itvm` `v'` `v`. If this is `Smaller`
or `Includes`, `v`' is smaller than `v` in preorder, so we have
found a valid node for the second case of the low-high order
definition. Greater and Included correspond to the cases
where `v`' is greater than `v` in preorder. If this is `Included`, `v`'
is a descendant of `v` in `T`, and it should be ignored. If this
is Greater, then we have found a valid node for the second
case of the low-high order definition.

Actually, we can go further in the analysis of case `Includes`.
In this case, by interval inclusion, `v`' is a strict ancestor of `v`
in `T`. But by the parent property, we also have that the parent
of `v` in `T` is an ancestor of `v`'. There is only one solution:
`v`' is the parent of `v` in `T`. This could be used to remove the
check that `v`' is the parent of `v` in `T`, and use only the inter-
vals, but experiments have shown that doing that degrades
performance.

## 3.4 Interface

If the check succeeds, we export three objects: the dominator
tree itself `dom_tree` (the result of `build`); the fast access
to the immediate dominator `idom` (the result of `make_D Fun`);
and the ancestor check that internally relies on interval in-
clusion `dom_test` (function `is_ancestor`), that was already
exported in [5].

Interestingly, the dominator tree and the fast access to
the immediate dominator were already computed in [5], but
used only as intermediate objects to perform the verification.
We now expose them as proper objects that other parts of
the compiler can use.

Four properties are proved about them.

Lemma `idom correct` : `forall` `n d`,
`clos_refl_trans` _ (`fun u v` ⇒ `idom u` = `Some v`) `n d`
↔ `dom d n`.
Lemma `dom_test correct`: `forall n d, reached n → dom_test d n = true ↔ dom d n.`

Lemma `idom_defined`: `forall u, idom u <> None ↔ get u code <> None ∧ u <> entry.`

Lemma `idom dom_tree`: `forall u v, idom u = Some v ↔ In u (sons dom_tree v)`.

Property `idom correct` states that the reflexive and transitive closure of `idom` is the dominance relation. Property `dom_test correct` states that the dominance test is sound and complete w.r.t. the dominance relation (for nodes reachable from entry). [5] proved only the direct sense, i.e. the soundness. We add the completeness. Property `idom defined` states that `idom` is defined on the nodes of the CFG code, except entry. Property `idom dom_tree` states that `idom` is intuitively the inverse of `dom_tree`.

# 4 Experiments

We prove stronger properties than the previous implementation, but this requires more computation, both on the OCaml side, to compute a low-high order, and on the Rocq side, to check that the order is low-high. We want to evaluate the cost of these additional calculations.

Since the old and the new implementations share some components, and to have a precise idea of the cost of each, we measured the time taken by each component separately. On the OCaml side, we measure the time taken by the construction of the dominator tree using the simple version of Lengauer-Tarjan (SLT), and the time taken by the computation of a low-high order (the version proved correct on paper by Georgiadis and Tarjan, LH, and the version conjectured correct, LHC). For SLT, we use the optimized and instrumented version described in Section 3.1. On the Rocq side, we measure the time needed to construct the intermediate objects described in Section 3.2 (OBJ) and the time needed by the checker itself (CHECKER). We consider 4 variants of the checker: the old and the new ones, both coming in two versions, the one using binary integers (type Z) as labels, and the one using the efficient primitive integers provided by Rocq (type Int63).

We exclude from the measurements the constructions of the CFG and of the reversed CFG, since both are already performed in the development version of CompCertSSA. The reversed CFG is used only by the new checker, not the old one, but it is already constructed for other purposes than computing dominators.

We perform the evaluations on a set of programs taken from CompCert's benchmarks. Experiments were performed on a Dell Latitude 7410 with an Intel Core i5-10310U processor at 1.70 GHz and 8 GB of memory. Since the programs are not that large, the execution time of each component can be really small. To mitigate that, we ran each component 1000 times in a row, and measured the cumulative time. Still, some of the programs are so small that the measured times

were still insignificant, so we ruled out the programs where the time taken by SLT was less than 0.03 s.

The results are presented in Table 2. For each program, we report its number of lines of code, and the time taken by the 1000 executions of each component, in seconds.

We can first observe that the building of a low-high order has a significant cost. On these programs, its execution time is between 1x and 3x the time of SLT. Using LHC rather than LH mitigates this, since the conjecture implementation appears to be much faster (sometimes twice as fast). Once again, this shows the strength of this certified approach. In the unverified part, experimenting with new implementations is easy.

On the Rocq side, the construction of the intermediate objects is costly too, up to twice as costly as SLT. As for the checkers, they run faster than SLT, but still have a non-negligible cost. Using primitive integers rather than Z helps significantly, for both checkers. Comparing the new checker to the old one, it turns out to run nearly as fast as its predecessor. Surprisingly, while it checks more things than the old one, it even outperforms it in some cases, e.g. bzip2 and nsichneu. A possible explanation of the good performance of the new checker in our case is that the considered programs likely have a simple control-flow. If, in a CFG, most of the nodes have only one predecessor, checking that the order is low-high is mostly trivial.

The last two columns present the times needed by the whole pipeline, in the old and new settings. In both cases, we consider the most efficient version. In the old setting, we sum SLT, OBJ and CHECKER (old, Int63). In the new setting, we sum SLT, LHC, OBJ and CHECKER (new, Int63). Clearly, the new approach is more expensive (around 50% more expensive), but it does not explode either. The difference comes mostly from the cost of LHC. The percentages given compare the times to SLT. It gives an idea of the price we pay to go from an unverified to a certified implementation. With the current implementations, the price is high. The old pipeline is 3 times as slow as SLT. The new one is between 4 and 5 times as slow. As mentioned in Section 3.1, it is likely that LH and LHC can be made faster, but probably not to the point of affecting the overall trend.

# 5 Conclusion and Perspectives

We have described the formalization and the implementation in the CompCertSSA verified compiler of a certifier of the dominator tree construction using a low-high order as a certificate, following the methodology described in [14]. This strengthens the previous implementation due to [5], proving completeness in addition to soundness. Experiments show that the new approach is more expensive, but still usable.

In the current implementation, the algorithm used to build the dominator tree is the simple version of the classic Lengauer-Tarjan algorithm. But the results are not limited
<table><caption>**Table 2.** Running times, in seconds, of 1000 runs of each component involved in the dominator tree certification. Total (old) is SLT + OBJ + CHECKER (old, Int63). Total (new) is SLT + LHC + OBJ + CHECKER (new, Int63). The percentages are relative to SLT.</caption><thead><tr><th rowspan="2">Program</th><th rowspan="2">LOC</th><th rowspan="2">SLT</th><th rowspan="2">LH</th><th rowspan="2">LHC</th><th rowspan="2">OBJ</th><th colspan="2">CHECK (old)</th><th colspan="2">CHECK (new)</th><th rowspan="2">Total (old)</th><th rowspan="2">Total (new)</th></tr><tr><th>Z</th><th>Int63</th><th>Z</th><th>Int63</th></tr></thead><tbody><tr><td>aes</td><td>1446</td><td>0.46</td><td>1.25</td><td>0.77</td><td>0.72</td><td>0.36</td><td>0.24</td><td>0.39</td><td>0.26</td><td>1.42 (309%)</td><td>2.21 (480%)</td></tr><tr><td>almabench</td><td>351</td><td>0.17</td><td>0.45</td><td>0.28</td><td>0.25</td><td>0.13</td><td>0.09</td><td>0.14</td><td>0.09</td><td>0.51 (300%)</td><td>0.79 (465%)</td></tr><tr><td>arcode</td><td>2463</td><td>0.23</td><td>0.52</td><td>0.31</td><td>0.34</td><td>0.2</td><td>0.13</td><td>0.22</td><td>0.14</td><td>0.70 (304%)</td><td>1.02 (443%)</td></tr><tr><td>bisect</td><td>377</td><td>0.06</td><td>0.11</td><td>0.06</td><td>0.1</td><td>0.06</td><td>0.04</td><td>0.06</td><td>0.04</td><td>0.20 (333%)</td><td>0.26 (433%)</td></tr><tr><td>bzip2</td><td>7007</td><td>6.71</td><td>21.05</td><td>12.26</td><td>10.88</td><td>5.33</td><td>3.37</td><td>5.32</td><td>3.16</td><td>20.96 (312%)</td><td>33.01 (492%)</td></tr><tr><td>chomp</td><td>364</td><td>0.05</td><td>0.16</td><td>0.1</td><td>0.07</td><td>0.04</td><td>0.03</td><td>0.05</td><td>0.03</td><td>0.15 (300%)</td><td>0.25 (500%)</td></tr><tr><td>fannkuch</td><td>154</td><td>0.03</td><td>0.05</td><td>0.03</td><td>0.05</td><td>0.03</td><td>0.02</td><td>0.03</td><td>0.02</td><td>0.10 (333%)</td><td>0.13 (433%)</td></tr><tr><td>fft</td><td>193</td><td>0.08</td><td>0.12</td><td>0.06</td><td>0.13</td><td>0.07</td><td>0.04</td><td>0.08</td><td>0.05</td><td>0.25 (312%)</td><td>0.32 (400%)</td></tr><tr><td>fftsp</td><td>198</td><td>0.09</td><td>0.13</td><td>0.06</td><td>0.15</td><td>0.08</td><td>0.05</td><td>0.09</td><td>0.05</td><td>0.29 (322%)</td><td>0.35 (389%)</td></tr><tr><td>knucleotide</td><td>376</td><td>0.07</td><td>0.16</td><td>0.09</td><td>0.11</td><td>0.06</td><td>0.04</td><td>0.07</td><td>0.04</td><td>0.22 (314%)</td><td>0.31 (443%)</td></tr><tr><td>lzss</td><td>2565</td><td>0.21</td><td>0.46</td><td>0.27</td><td>0.28</td><td>0.17</td><td>0.11</td><td>0.2</td><td>0.12</td><td>0.60 (286%)</td><td>0.88 (419%)</td></tr><tr><td>lzw</td><td>2302</td><td>0.19</td><td>0.41</td><td>0.24</td><td>0.26</td><td>0.16</td><td>0.1</td><td>0.18</td><td>0.11</td><td>0.55 (289%)</td><td>0.80 (421%)</td></tr><tr><td>mcf</td><td>2045</td><td>0.4</td><td>0.88</td><td>0.51</td><td>0.58</td><td>0.34</td><td>0.21</td><td>0.4</td><td>0.23</td><td>1.19 (298%)</td><td>1.72 (430%)</td></tr><tr><td>nbody</td><td>174</td><td>0.04</td><td>0.09</td><td>0.05</td><td>0.06</td><td>0.03</td><td>0.02</td><td>0.03</td><td>0.02</td><td>0.12 (300%)</td><td>0.17 (425%)</td></tr><tr><td>nsichneu</td><td>4033</td><td>5.28</td><td>8.66</td><td>4.71</td><td>9.55</td><td>4.14</td><td>2.62</td><td>3.57</td><td>2.09</td><td>17.45 (330%)</td><td>21.63 (410%)</td></tr><tr><td>perlin</td><td>77</td><td>0.07</td><td>0.1</td><td>0.05</td><td>0.11</td><td>0.06</td><td>0.04</td><td>0.06</td><td>0.04</td><td>0.22 (314%)</td><td>0.27 (386%)</td></tr><tr><td>raytracer</td><td>2568</td><td>1.38</td><td>3.47</td><td>1.98</td><td>1.96</td><td>1.11</td><td>0.71</td><td>1.27</td><td>0.78</td><td>4.05 (293%)</td><td>6.10 (442%)</td></tr><tr><td>sha1</td><td>236</td><td>0.05</td><td>0.11</td><td>0.06</td><td>0.08</td><td>0.04</td><td>0.03</td><td>0.05</td><td>0.03</td><td>0.16 (320%)</td><td>0.22 (440%)</td></tr><tr><td>sha3</td><td>223</td><td>0.2</td><td>0.48</td><td>0.28</td><td>0.3</td><td>0.15</td><td>0.1</td><td>0.16</td><td>0.11</td><td>0.60 (300%)</td><td>0.89 (445%)</td></tr><tr><td>siphash24</td><td>256</td><td>0.11</td><td>0.3</td><td>0.19</td><td>0.15</td><td>0.08</td><td>0.05</td><td>0.09</td><td>0.06</td><td>0.31 (282%)</td><td>0.51 (464%)</td></tr><tr><td>spass</td><td>69081</td><td>84.37</td><td>259.18</td><td>156.31</td><td>130.22</td><td>66.06</td><td>41.94</td><td>69.33</td><td>42.78</td><td>256.53 (304%)</td><td>413.68 (490%)</td></tr><tr><td>vmach</td><td>211</td><td>0.05</td><td>0.07</td><td>0.03</td><td>0.07</td><td>0.04</td><td>0.02</td><td>0.05</td><td>0.03</td><td>0.14 (280%)</td><td>0.18 (360%)</td></tr></tbody></table>

to this algorithm. This is the advantage of the certified approach: any algorithm building a dominator tree and producing a low-high order can replace the current implementation, without any impact on the rest of the compiler.

This work should enable the formalization of new algorithms based on dominance, either those requiring completeness (including [16, 17] mentioned in Section 1), or those working directly on the dominator tree that was not exposed before. New formalizations could reveal possible improvements to the exposed interface.

One limitation of the certified approach is the price we pay in performance w.r.t. the base algorithm. Experiments have shown that it is high. This may be a sufficient motivation to try a direct proof of the Lengauer-Tarjan algorithm.

## Acknowledgments

I thank David Pichardie for discussing the theory and the preliminary version of this paper. I thank Sandrine Blazy and Delphine Demange for pushing me to write this article. I also thank Lionel Blatter, Paolo Torrini and Benjamin Grégoire for their feedback on drafts of this paper. Finally, I thank the anonymous reviewers for their comments.

## References

[1] Frances E. Allen and John Cocke. 1972. *Graph-theoretic constructs for program control flow analysis*. Technical Report IBM Res. Rep. RC 3923. IBM T.J. Watson Research Center.

[2] Andrew W. Appel and Xavier Leroy. 2023. Efficient Extensional Binary Tries. *J. Autom. Reason*. 67, 1 (2023), 8. doi:10.1007/S10817-022-09655-X

[3] Andrew W. Appel and Jens Palsberg. 2002. *Modern Compiler Implementation in Java, 2nd edition*. Cambridge University Press.

[4] Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. *ACM Trans. Program. Lang. Syst*. 36, 1 (2014), 4:1–4:35. doi:10.1145/2579080

[5] Sandrine Blazy, Delphine Demange, and David Pichardie. 2015. Validating Dominator Trees for a Fast, Verified Dominance Test. In *Intercative Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (Lecture Notes in Computer Science, Vol. 9236)*, Christian Urban and Xingyuan Zhang (Eds.). Springer, 84–99. doi:10.1007/978-3-319-22102-1_6

[6] Adam L. Buchsbaum, Loukas Georgiadis, Haim Kaplan, Anne Rogers, Robert Endre Tarjan, and Jeffery R. Westbrook. 2008. Linear-Time Algorithms for Dominators and Other Path-Evaluation Problems. *SIAM J. Comput*. 38, 4 (2008), 1533–1573. doi:10.1137/070693217

[7] Keith D. Cooper, Timothy J. Harvey, and Ken Kennedy. 2006. *A Simple, Fast Dominance Algorithm*. Technical Report TR-06-38870. Rice University.

[8] Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. *Introduction to Algorithms, 3rd Edition*. MIT Press. http://mitpress.mit.edu/books/introduction-algorithms

[9] Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. *ACM Trans. Program.*
Lang. Syst. 13, 4 (1991), 451–490. doi:10.1145/115372.115320

[10] Wojciech Fraczak, Loukas Georgiadis, Andrew Miller, and Robert Endre Tarjan. 2013. Finding dominators via disjoint set union. *J. Discrete Algorithms* 23 (2013), 2–20. doi:10.1016/J.JDA.2013.10.003
Corrections in 26 (2014), 106–110.

[11] Loukas Georgiadis, Luigi Laura, Nikos Parotsidis, and Robert Endre Tarjan. 2013. Dominator Certification and Independent Spanning Trees: An Experimental Study. In *Experimental Algorithms, 12th International Symposium, SEA 2013, Rome, Italy, June 5-7, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7933)*, Vincenzo Bonifaci, Camil Demetrescu, and Alberto Marchetti-Spaccamela (Eds.). Springer, 284–295. doi:10.1007/978-3-642-38527-8_26

[12] Loukas Georgiadis and Nikos Parotsidis. 2013. Dominators in Directed Graphs: A Survey of Recent Results, Applications, and Open Problems. In *2nd International Symposium on Computing in Informatics and Mathematics (ISCIM 2013)*. 15–20.

[13] Loukas Georgiadis and Robert E. Tarjan. 2016. Addendum to "Dominator Tree Certification and Divergent Spanning Trees". *ACM Trans. Algorithms* 12, 4 (2016), 56:1–56:3. doi:10.1145/2928271

[14] Loukas Georgiadis and Robert E. Tarjan. 2016. Dominator Tree Certification and Divergent Spanning Trees. *ACM Trans. Algorithms* 12, 1 (2016), 11:1–11:42. doi:10.1145/2764913

[15] Loukas Georgiadis, Robert Endre Tarjan, and Renato Fonseca F. Werneck. 2006. Finding Dominators in Practice. *J. Graph Algorithms Appl.* 10, 1 (2006), 69–94. doi:10.7155/JGAA.00119

[16] Yann Herklotz, Delphine Demange, and Sandrine Blazy. 2023. Mechanised Semantics for Gated Static Single Assignment. In *Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 182–196. doi:10.1145/3573105.3575681

[17] Jean-Christophe Léchenet, Sandrine Blazy, and David Pichardie. 2020. A Fast Verified Liveness Analysis in SSA Form. In *Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 12167)*, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer, 324–340. doi:10.1007/978-3-030-51054-1_19

[18] Thomas Lengauer and Robert Endre Tarjan. 1979. A Fast Algorithm for Finding Dominators in a Flowgraph. *ACM Trans. Program. Lang. Syst.* 1, 1 (1979), 121–141. doi:10.1145/357062.357071

[19] Xavier Leroy. 2009. A Formally Verified Compiler Back-end. *J. Autom. Reason.* 43, 4 (2009), 363–446. doi:10.1007/S10817-009-9155-4

[20] Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert – A Formally Verified Optimizing Compiler. In *ERTS 2016: Embedded Real Time Software and Systems*. SEE. http://xavierleroy.org/publi/erts2016_compcert.pdf

[21] Jean-Christophe Léchenet. 2025. Artefact for "Mechanized Dominator Tree Certification", *CPP 2026*. doi:10.5281/zenodo.17795214

[22] Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In *Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012*, John Field and Michael Hicks (Eds.). ACM, 427–440. doi:10.1145/2103656.2103709

[23] Jianzhou Zhao and Steve Zdancewic. 2012. Mechanized Verification of Computing Dominators for Formalizing Compilers. In *Certified Programs and Proofs - Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7679)*, Chris Hawblitzel and Dale Miller (Eds.). Springer, 27–42. doi:10.1007/978-3-642-35308-6_6

Received 2025-09-13; accepted 2025-11-13