The directory includes source code for the CPP12 submission.
1) cfg.v
Basic definitions and properties of control-flow-graphs: vertices, arcs,
successors, reachability and dominance.
2) reach.v
Metatheory of reachablity.
3) dom_decl.v
Metatheory of dominance.
4) dom_type.v
The specification of dominance algorithm.
5) dom_set.v
The Correctness of the AC algorithm.
6) dom_libs.v
Definitions and properties used by the CHK algorithm.
7) dfs.v
Depth-first-search.
7) push_iter.v
The low-level design and metatheory of CHK algorithm.
8) dom_list.v
The Correctness of the CHK algorithm.
9) dom_tree.v
Basic definitions and properties of dominator trees constructions.
10) dom_list_tree.v
The correctness of CHK-tree algorithm.
11) dom_set_tree.v
The implementation of AC-tree algorithm. Note: we did not prove the correct
of AC-tree fully. We implemented the algorithm to compare its performance
with CHK-tree.
Misc:
1) pull_iter.v
This is an implementation of Kildall that, at each iteration, pulls
information from the predeccessors of a node to the node. The Kildall
algorithm we use push information from a node to its successors at each
iteration. We implemented pull_iter.v to evaluate some design trade-offs of
Kildall, do not present pull_iter.v in our paper submission.
2) cpdt_tactics.v
Tactics copied from Adam Chlipala's book.