Dominator tree certification and divergent spanning trees
From MaRDI portal
Abstract: 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.
Recommendations
Cited in
(18)- 2-vertex connectivity in directed graphs
- Sparse certificates for 2-connectivity in directed graphs
- Approximating the smallest 2-vertex connected spanning subgraph of a directed graph
- Dominators, directed bipolar orders, and independent spanning trees
- Dominator tree verification and vertex-disjoint paths
- Validating dominator trees for a fast, verified dominance test
- 2-vertex connectivity in directed graphs
- scientific article; zbMATH DE number 4011953 (Why is no real title available?)
- A Fast Verified Liveness Analysis in SSA Form
- Minimum 2-vertex strongly biconnected spanning directed subgraph problem
- Dynamic Dominators and Low-High Orders in DAGs
- Strong connectivity in directed graphs under failures, with applications
- Polylogarithmic Approximation Algorithm for k-Connected Directed Steiner Tree on Quasi-Bipartite Graphs
- Efficient computation of arbitrary control dependencies
- Efficient certifying algorithms for linear classification
- A combinatorial certifying algorithm for linear programming problems with gainfree Leontief substitution systems
- Higher connectivity in directed graphs (invited talk)
- A combinatorial certifying algorithm for linear programming problems with gainfree Leontief substitution systems
This page was built for publication: Dominator tree certification and divergent spanning trees
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4962208)
