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.