Learning-aided Program Reasoning

软件是我们现代数字世界的基石。然而，开发可靠的软件是众所周知的挑战。一个无意的编程错误（例如Heartbleed漏洞）可能会使数百万的Web服务器容易受到攻击。为了系统地消除软件漏洞，研究团体和工业实验室已经开发了许多程序推理工具。不幸的是，为了实现可用的准确性和可扩展性，这些程序推理工具必须为每个代码库进行仔细定制，这需要非平凡的专业知识，限制了普通软件开发人员的采用。培训（或简单地招聘）高技能的程序员，换句话说，“人类学习”是缓解这些问题的传统和工业方法，然而，这是缓慢的，昂贵的，不可扩展的。该计划旨在开发一种经济，可扩展和易于访问的方法，可以同时帮助数十万真实世界的程序员。关键的见解是让编程环境本身积极地从过去的执行、错误、补丁、历史版本和其他类似的软件存储库中学习。 该计划的主要目标是研究机器学习或更一般的人工智能（AI）如何帮助改善软件开发各个阶段的编程推理。我们将设计和构建一个智能编程助手，它可以从大型软件存储库中学习，捕捉各种错误，并在运行中建议习惯用法和补丁，并用可学习的组件来取代手动设计的分析和测试规则，这些组件会随着时间的推移逐渐适应给定的代码库。特别是，该计划将集中在三个目标：1）通过挖掘习惯用法和规范来改善语法级推理，2）通过学习规则和放松规则来改善静态推理; 3）通过学习有效的神经策略来改善动态推理指导动态符号执行。 拟议的研究将显着推进最先进的编程推理技术，由此产生的工具链将免费提供，并易于访问的平均软件开发人员。该计划将培养10名高素质人才（HQP），包括2名博士，3名硕士和5名本科生，在编程语言，软件工程和机器学习的跨学科领域。HQP将获得构建“大代码”处理管道，设计程序分析和合成算法以及机器学习模型，开发实用软件分析和测试工具链以及进行用户研究和大规模评估的实践经验。这些技能为HQP在跨学科研究领域和软件行业取得巨大成功奠定了坚实的基础。

Software forms the cornerstone of our modern digital world. However, developing reliable software is notoriously challenging. An inadvertent programming mistake (e.g. Heartbleed bug) could make millions of web servers vulnerable. To systematically eliminate software vulnerabilities, many program reasoning tools have been developed by research communities and industrial labs. Unfortunately, in order to achieve a usable accuracy and scalability, these program reasoning tools have to be carefully customized for each codebase, which requires non-trivial expertise, limiting their adoption by average software developers. Training (or simply recruiting) highly-skilled programmers, in other words, "human learning", is the conventional and industrial way to mitigate these issues, which is however slow, expensive, and non-scalable. The proposed program aims to develop an economical, scalable and easily accessible approach, which can assist hundreds of thousands of real-world programmers at once. The key insight is to make the programming environment itself actively learn from past executions, mistakes, patches, historical versions, and other similar software repositories. The main goal of this program is to investigate how machine learning, or more generally artificial intelligence (AI), can help to improve programming reasoning in various stages of software development. We will design and build an intelligent programming assistant, which learns from large software repositories, catches various mistakes and suggests idioms and patches on the fly, and which replaces manually designed heuristics or rules for analysis and testing with learnable components that gradually adapt to given codebase overtime. Particularly, the proposed program will focus on three objectives: 1) improving syntactic-level reasoning by mining idioms and specifications, 2) improving static reasoning by learning rules and relaxing rules with numerical weights; 3) improving dynamic reasoning by learning an effective neural-policy guiding dynamic symbolic execution. The proposed research will significantly advance state-of-the-art programming reasoning techniques and the resulting toolchain will be freely available and easily accessible to average software developers. This program will train 10 Highly Qualified Personnel (HQP), including 2 PhDs, 3 MSc and 5 undergraduate students, in the interdisciplinary areas of programming languages, software engineering, and machine learning. HQP will gain hands-on experience of building a "big code" processing pipeline, designing program analysis and synthesis algorithms and machine learning models, developing practical software analysis and testing toolchain, and conducting user studies and large-scale evaluations. These skills form a solid background for HQP to achieve great successes in the interdisciplinary area of research as well as software industry.