CAREER: Cooperative Program Analysis: Bridging the Gap Between User and Tool Reasoning

虽然不是完美的，但今天的自动化分析工具能够计算出关于程序的深度和广度确实是了不起的。然而，尽管软件缺陷的普遍性和成本，尽管这种自动化工具可以提供丰富的信息，程序分析器在很大程度上被当今的软件工程师忽视。这种情况不是由于软件工程师缺乏兴趣或分析专家在部署方面缺乏努力，而是由于工具及其用户对程序的原因的方式存在差距，这导致例如在提供用户可理解的分析结果方面存在困难。这项研究面临着弥合这一用户-工具推理鸿沟的问题。工作的重点是一种有效的用户驱动的分析过程精化方法。将创建用于生成程序分析结果的解释的新技术。将开发新的方法来权衡编译时验证的穷举性和运行时检查的简单性。这个项目与以前在以用户为中心的分析规范方面的工作一起，为未来的工具奠定了基础，在这些工具中，用户和工具可以合作有效地对程序进行推理。重大的潜在影响包括：软件工程师看待程序分析的方式的改变--用透明的推理助手取代魔盒，由于这种观点的改变而提高了软件质量，以及以动手的方式吸引学生进行算法思考的工具。

While not perfect, the depth and breadth of what today's automated analysis tools can figure out about a program is truly remarkable. Yet, despite the prevalence and cost of software defects and despite the wealth of information such automated tools could provide, program analyzers are largely ignored by today's software engineers. This situation is not due to a lack of interest from software engineers or a lack of effort in deployment from analysis experts but rather a gap in the way a tool and its user reasons about the program, which results in, for example, a difficulty in providing analysis results understandable to the user. This research confronts closing this user-tool reasoning gap.The focus of the work is an effective approach to user-driven refinement of the analysis process. Novel techniques for generating explanations of program analysis results will be created. New approaches for trading off the exhaustiveness of compile-time verification and the simplicity of run-time checking will be developed. Together with prior work on user-centric analysis specifications, this project lays the foundation for tomorrow's tools where users and tools cooperate to reason effectively about programs. Significant potential impacts include the following: a change in the way software engineers view program analysis--replacing a magic box with a transparent reasoning assistant, improved software quality as a result of this change in view, and tools that engage students in algorithmic thinking in a hands-on manner.