A successful automated program proof is, in software verification, the ultimate triumph. In practice, however, the road to such success is paved with many failed proof attempts. If a proof fails, the prover usually gives little useful feedback, making it very hard to know how to proceed. 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): if the proof fails, it transforms the counterexample model generated by the prover to a user-friendly format; counterexamples can be further simplified by reducing the containing integer values to their minimal possible. We have implemented the CEAM approach as an extension in the AutoProof verifier and demonstrate its application on a collection of examples.
翻译:成功的自动程序验证在软件核查中是最终的胜利。 但在实践中, 成功的道路是被许多失败的验证尝试所铺设的。 如果证明失败, 证明人通常很少提供有用的反馈, 很难知道如何进行。 此处报告的工作试图通过提供可以立即理解的反实例来帮助处理这类案例。 为此, 它引入了一种名为 " 反采掘和最小化(CEAM) " 的方法: 如果证明失败, 它将把验证人产生的反样模型转换成一种方便用户的格式; 将包含的整数值减少到尽可能的最低限度, 反样例可以进一步简化。 我们已经将CEAM方法作为AutoProof 校验器的延伸, 并演示其在收集实例方面的应用 。