论文标题
通过失败的程序验证提高反例质量
Improving Counterexample Quality from Failed Program Verification
论文作者
论文摘要
在软件验证中，成功的自动化程序证明是最终的胜利。但是，通往这种成功的道路是许多失败的证明尝试铺平的。当证明失败的情况通常晦涩时，供奉献者产生的信息通常很难知道如何进一步进行。这里报告的工作试图通过立即提供可理解的反例来帮助在这种情况下提供帮助。 为此，它引入了一种称为反例提取和最小化（CEAM）的方法。当证明失败时，CEAM将供奉献者生成的反例模型变成一个明显可理解的版本。另外，它可以通过最小化其包含的整数值来进一步简化反例。我们已经实施了CEAM方法，以扩展自动置验证仪，并演示了其应用于示例集合的应用。
In software verification, a successful automated program proof is the ultimate triumph. The road to such success is, however, paved with many failed proof attempts. The message produced by the prover when a proof fails is often obscure, making it very hard to know how to proceed further. The work reported here attempts to help in such cases by providing immediately understandable counterexamples. To this end, it introduces an approach called Counterexample Extraction and Minimization (CEAM). When a proof fails, CEAM turns the counterexample model generated by the prover into a a clearly understandable version; it can in addition simplify the counterexamples further by minimizing the integer values they contain. We have implemented the CEAM approach as an extension to the AutoProof verifier and demonstrate its application to a collection of examples.
