支配树认证与独立生成树

如何验证复杂程序的输出是否正确？人们可以形式化地证明程序是正确的，但这可能超出了现有方法的能力范围。或者，可以通过在输入 - 输出对上运行检查器，来检查为特定输入产生的输出是否满足所需的输入 - 输出关系。此时只需证明检查器的正确性。但对于某些问题，即使是这样的检查器也可能过于复杂而难以形式化验证。还有第三种选择：增强原始程序，使其不仅产生输出，还产生一个正确性证书，使得一个非常简单的程序（其正确性易于证明）能够利用该证书来验证输入 - 输出对是否满足所需的输入 - 输出关系。我们考虑这个一般问题的一个重要实例：如何验证流图的支配树是否正确？现有的寻找支配者的快速算法非常复杂，甚至在没有额外信息的情况下验证支配树的正确性似乎也很复杂。我们定义了支配树的正确性证书，展示了如何利用它轻松验证树的正确性，并展示了如何增强快速支配者查找算法以使其产生正确性证书。我们还将支配证书问题与在流图中寻找独立生成树的问题联系起来，并开发了寻找此类树的算法。我们所有的算法都在线性时间内运行。先前的算法仅适用于仅有平凡支配者的特殊情况，且至少需要二次时间。