在大型Source Code Haystacks中发现模型可检查的针：通过静态分析和动态不变发现的模块化错误发现
Finding Model-Checkable Needles in Large Source Code Haystacks: Modular Bug-Finding via Static Analysis and Dynamic Invariant Discovery
摘要：
在本文中，我们提出了一种新的婚姻的静态和动态分析。给定具有许多功能的大型代码库和成熟的测试套件，我们建议使用静态分析来找到具有断言或其他明显正确性属性的功能1）（例如，数组边界要求或指针访问），以及2）具有足够简单的控制流和数据使用，以服从基于谓词抽象或有界模型检验，而无需人工干预。由于大多数这样的功能在现实的软件系统中，实际上依赖于许多输入的前提条件，而不是指定的语言的类型系统（或以任何方式注释），我们建议使用动态发现的不变量的基础上，程序的测试套件，以表征可能的前提条件，以减少误报的问题。虽然在验证方面提供的很少，但这种方法可以为通常被认为“太大而无法进行模型检查”的程序提供额外的快速和高度可扩展的错误查找方法。“我们提出了一个简单的例子，表明该技术可以用于更典型的“模型可检查”的代码库，即使在存在设计不良的测试套件和坏的不变量。
英文摘要：
In this paper, we present a novel marriage of static and dynamic analysis. Given a large code base with many functions and a mature test suite, we propose using static analysis to find functions 1) with assertions or other evident correctness properties (e.g., array bounds requirements or pointer access) and 2) with simple enough control flow and data use to be amenable to predicate-abstraction based or bounded model checking without human intervention. Because most such functions in realistic software systems in fact rely on many input preconditions not specified by the language's type system (or annotated in any way), we propose using dynamically discovered invariants based on a program's test suite to characterize likely preconditions, in order to reduce the problem of false positives. While providing little in the way of verification, this approach may provide an additional quick and highly scalable bug-finding method for programs that are usually considered "too large to model check." We present a simple example showing that the technique can be useful for a more typically "model-checkable" code base, even in the presence of a poorly designed test suite and bad invariants.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
