SHF: Small: Collaborative Research: Dynamic Invariant Inference, Enhanced

SHF：小型：协作研究：动态不变推理，增强型

• 批准号: 0917391
• 负责人: Michal Young
• 金额: $ 16.7万
• 依托单位: University of Oregon Eugene
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-09-01 至 2012-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0917391&HistoricalAwards=false
• 关键词: SHF; Small; Collaborative; Research; Dynamic

In just a decade, dynamic invariant inference has emerged as one of the most promising directions in program analysis, with a variety of applications. An invariant inference system observes a program during test execution and filters a large number of candidate invariants (i.e., suspected relations between program data), finally reporting only those that hold with high confidence. However, inferred invariants are not always true (they depend on the quality of a test suite), and the few really useful invariants discovered are often accompanied by many more true but trivial and irrelevant facts. This work improves the quality of discovered invariants by ensuring their consistency with facts that are known statically. For instance, even though the invariants describing the behavior of two functions f1 and f2 may be unknown, we may know that any valid input for f1 is also valid for f2. This fact can be incorporated in the inference process to eliminate inconsistent invariants. More generally, the work explores techniques for expressing, discovering, and employing such consistency constraints to improve the quality of produced invariants, from type information and other sources including static analysis and user-supplied annotation.The work will impact many aspects of software engineering, including scientific and industrial uses. Concrete benefits will be in the form of publications, usable software (released under an academic open-source license), software prototypes, and educational activities and resources (enhancement of a textbook and current courses, internships for high school students).

在短短的十年里，动态不变推理已经成为程序分析中最有前途的方向之一，具有各种应用。不变量推理系统在测试执行期间观察程序并过滤大量候选不变量（即，程序数据之间的可疑关系），最后只报告那些具有高置信度的关系。然而，推断的不变量并不总是正确的（它们取决于测试套件的质量），并且发现的少数真正有用的不变量通常伴随着许多更真实但琐碎和不相关的事实。这项工作通过确保它们与静态已知事实的一致性来提高发现的不变量的质量。例如，即使描述两个函数f1和f2的行为的不变量可能是未知的，我们也可以知道f1的任何有效输入对f2也是有效的。这个事实可以被合并到推理过程中，以消除不一致的不变量。更一般地说，这项工作探索了表达，发现和使用这种一致性约束的技术，以提高从类型信息和其他来源（包括静态分析和用户提供的注释）产生的不变量的质量。这项工作将影响软件工程的许多方面，包括科学和工业用途。具体的好处将体现在出版物、可用软件（在学术开源许可证下发布）、软件原型以及教育活动和资源（改进教科书和当前课程、高中生实习）。