论文标题
谁验证验证者？ DAFNY中DPLL算法的计算机检查的实现
Who Verifies the Verifiers? A Computer-Checked Implementation of the DPLL Algorithm in Dafny
论文作者
论文摘要
我们在启用验证的编程语言DAFNY中构建了一个实现DPLL算法的SAT求解器。最终的求解器已充分验证（计算机检查了声音，完整性和终止）。我们基于DAFNY求解器基准测试，我们证明它与C＃中实现的等效DPLL求解器一样有效，效率大约是C ++编写的等效求解器的效率。我们得出的结论是，自动验证是增加对SAT求解器信任的有前途的方法，因为它结合了执行速度和最终产品的可信度程度之间的良好权衡。
We build a SAT solver implementing the DPLL algorithm in the verification-enabled programming language Dafny. The resulting solver is fully verified (soundness, completeness and termination are computer checked). We benchmark our Dafny solver and we show that it is just as efficient as an equivalent DPLL solver implemented in C# and roughly two times less efficient than an equivalent solver written in C++. We conclude that auto-active verification is a promising approach to increasing trust in SAT solvers, as it combines a good trade-off between execution speed and degree of trustworthiness of the final product.
