有界模型检验与特征遗漏多样性
Bounded Model Checking and Feature Omission Diversity
摘要：
在本文中，我们介绍了一种新的方法，以加快发现的反例有界模型检验，基于并行运行的系统中的功能已被随机禁用的版本。如前所述，在有界模型检验问题中加入约束可以减小验证问题的规模，并大大减少寻找反例所需的时间。在软件测试中开发的技术适用于这个问题，提供了一种简单的方法来产生有用的部分验证问题，从而减少了产生反例的平均时间。如果没有找到反例，部分验证结果也可以在实践中使用。
英文摘要：
In this paper we introduce a novel way to speed up the discovery of counterexamples in bounded model checking, based on parallel runs over versions of a system in which features have been randomly disabled. As shown in previous work, adding constraints to a bounded model checking problem can reduce the size of the verification problem and dramatically decrease the time required to find counterexample. Adapting a technique developed in software testing to this problem provides a simple way to produce useful partial verification problems, with a resulting decrease in average time until a counterexample is produced. If no counterexample is found, partial verification results can also be useful in practice.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
