中间体验证剂的耐用性检测
Robustness Testing of Intermediate Verifiers
摘要：
程序验证器也不能避免几乎影响每一个软件的bug。此外，它们经常表现出脆弱的行为：它们的性能随着输入程序如何表达的细节而发生显著变化，这些细节应该是无关紧要的，比如独立声明的顺序。这种健壮性的缺乏使用户感到沮丧，他们必须花费大量的时间来弄清楚工具的特性，然后才能有效地使用它。本文介绍了一种技术来检测缺乏程序验证器的鲁棒性，该技术是轻量级的，全自动的，因为它是基于测试方法（如突变测试和变形测试）。其关键思想是生成最初通过验证的程序的许多简单变体。通过构造，所有变体都等同于原始程序;因此，任何未通过验证的变体都表明验证器缺乏鲁棒性。我们实现了我们的技术在一个工具，称为“mugie”，它的操作程序写在流行的布吉语言验证作为中间表示在众多的程序验证。针对135个Boogie程序的实验表明，脆性行为发生得相当频繁（16个程序），并且不难触发。基于这些结果，本文讨论了脆性行为的主要来源，并提出了提高鲁棒性的措施。
英文摘要：
Program verifiers are not exempt from the bugs that affect nearly every piece of software. In addition, they often exhibit brittle behavior: their performance changes considerably with details of how the input program is expressed-details that should be irrelevant, such as the order of independent declarations. Such a lack of robustness frustrates users who have to spend considerable time figuring out a tool's idiosyncrasies before they can use it effectively. This paper introduces a technique to detect lack of robustness of program verifiers; the technique is lightweight and fully automated, as it is based on testing methods (such as mutation testing and metamorphic testing). The key idea is to generate many simple variants of a program that initially passes verification. All variants are, by construction, equivalent to the original program; thus, any variant that fails verification indicates lack of robustness in the verifier. We implemented our technique in a tool called "mugie", which operates on programs written in the popular Boogie language for verification-used as intermediate representation in numerous program verifiers. Experiments targeting 135 Boogie programs indicate that brittle behavior occurs fairly frequently (16 programs) and is not hard to trigger. Based on these results, the paper discusses the main sources of brittle behavior and suggests means of improving robustness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
