多属性设计的高效验证（错误假设的好处）（扩展版）
计算机科学中的逻辑
2018-03-12 v2
摘要
我们考虑高效检查一个设计的若干安全性质 P1,....,Pk 的问题。我们引入一种称为 JA-验证的新方法，其中 JA 代表“Just-Assume”（相对于“假设-保证”）。在该方法中，当证明性质 Pi 时，假设所有 j!=i 的性质 Pj 均成立。证明性质的过程要么得出 P1,....,Pk 在无任何假设下均成立，要么找到一个性质的“调试集”。后者识别出导致其他性质失败的一组失败性质子集。必须首先修复导致调试集中性质失败的设计行为。重要的是，在我们的方法中，无需证明所用假设。我们描述了该方法背后的理论，并报告了实验结果显示出性能的实质性提升，尤其在存在较小调试集的情况下。
引用
@article{arxiv.1711.05698,
title = {Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)},
author = {Eugene Goldberg and Matthias Gudemann and Daniel Kroening and Rajdeep Mukherjee},
journal= {arXiv preprint arXiv:1711.05698},
year = {2018}
}
备注
6 pages, Design Automation and Test in Europe conference