  How does one verify that the output of a complicated program is correct? One
can formally prove that the program is correct, but this may be beyond the
power of existing methods. Alternatively one can check that the output produced
for a particular input satisfies the desired input-output relation, by running
a checker on the input-output pair. Then one only needs to prove the
correctness of the checker. But for some problems even such a checker may be
too complicated to formally verify. There is a third alternative: augment the
original program to produce not only an output but also a correctness
certificate, with the property that a very simple program (whose correctness is
easy to prove) can use the certificate to verify that the input-output pair
satisfies the desired input-output relation.
  We consider the following important instance of this general question: How
does one verify that the dominator tree of a flow graph is correct? Existing
fast algorithms for finding dominators are complicated, and even verifying the
correctness of a dominator tree in the absence of additional information seems
complicated. We define a correctness certificate for a dominator tree, show how
to use it to easily verify the correctness of the tree, and show how to augment
fast dominator-finding algorithms so that they produce a correctness
certificate. We also relate the dominator certificate problem to the problem of
finding independent spanning trees in a flow graph, and we develop algorithms
to find such trees. All our algorithms run in linear time. Previous algorithms
apply just to the special case of only trivial dominators, and they take at
least quadratic time.
