SHF:Large:Collaborative Research: Inferring Software Specifications from Open Source Repositories by Leveraging Data and Collective Community Expertise

今天，个人、社会和国家都严重依赖软件来管理电力、银行和金融、空中交通管制、电信、交通、国防和医疗保健等关键基础设施。规范对于将软件系统的预期行为传达给软件开发人员和用户以及使自动化工具能够验证给定软件是否确实按预期运行至关重要。安全关键应用传统上享受这种规范的好处，但成本很高。 由于从头开始产生有用的、非平凡的规范太难、太耗时，而且需要的专业知识并不广泛，因此这样的规范在很大程度上是不可用的。核心库和广泛使用的框架缺乏规范，使得指定使用它们的应用程序变得更加困难。缺乏精确的、可理解的和有效的可验证的规范是开发可靠的、安全的、易于维护和重用的软件系统的主要障碍。该项目汇集了一个跨学科的研究人员团队，他们在正式方法，软件工程，机器学习和大数据分析方面具有互补的专业知识，以开发自动或半自动的方法来从代码中推断规范。由此产生的方法和工具结合联合收割机分析大型开源代码库，以增强和改进规范的程序分析为基础的规范推理，通过协同进步，在这两个领域。该项目更广泛的影响包括：规范推理和综合方面的变革性进展，有可能大幅降低开发和维护高保证软件的成本;在正式方法软件工程和大数据分析的交叉点上增强跨学科专业知识;为具有高保证软件专业知识的科学家和工程师骨干的研究培训做出贡献。

Today individuals, society, and the nation critically depend on software to manage critical infrastructures for power, banking and finance, air traffic control, telecommunication, transportation, national defense, and healthcare. Specifications are critical for communicating the intended behavior of software systems to software developers and users and to make it possible for automated tools to verify whether a given piece of software indeed behaves as intended. Safety critical applications have traditionally enjoyed the benefits of such specifications, but at a great cost. Because producing useful, non-trivial specifications from scratch is too hard, time consuming, and requires expertise that is not broadly available, such specifications are largely unavailable. The lack of specifications for core libraries and widely used frameworks makes specifying applications that use them even more difficult. The absence of precise, comprehensible, and efficiently verifiable specifications is a major hurdle to developing software systems that are reliable, secure, and easy to maintain and reuse. This project brings together an interdisciplinary team of researchers with complementary expertise in formal methods, software engineering, machine learning and big data analytics to develop automated or semi-automated methods for inferring the specifications from code. The resulting methods and tools combine analytics over large open source code repositories to augment and improve upon specifications by program analysis-based specification inference through synergistic advances across both these areas. The broader impacts of the project include: transformative advances in specification inference and synthesis, with the potential to dramatically reduce, the cost of developing and maintaining high assurance software; enhanced interdisciplinary expertise at the intersection of formal methods software engineering, and big data analytics; Contributions to research-based training of a cadre of scientists and engineers with expertise in high assurance software.