Learning-aided Program Reasoning

点击翻译按钮获取中文摘要

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.