CAREER: Foundations of Statistical Program Reasoning

该奖项全部或部分由《2021年美国救援计划法案》（公法117-2）资助。程序分析和验证系统在设计上具有挑战性，在操作上也很昂贵，并且以可伸缩性差、错误警告和遗漏错误而闻名。此外，这些程序推理工具与现代软件工程过程的连续性和迭代性互操作很差，并且只有与人类工程师交互的基本方法。该项目开发了一些技术，以扩展这些分析的潜在演绎基础——通常使用声明式形式表达，如约束Horn子句（CHCs）或Datalog——采用概率推理模式。这些概率模型提供了一种机制来确定警告的优先级，合并来自开发人员的反馈，并结合来自多个分析工具的知识。因此，该项目的主要影响是显著提高程序分析技术的准确性和可用性。该项目开发算法，从实施分析中自动学习概率模型，并使用开源代码语料库（如GitHub）和数据库（如Common Vulnerabilities and Exposures， CVE）确定其准确性。接下来，它开发了排序技术，以优化有效的准确性、发现bug所需的时间和其他程序员指定的相关标准。该项目为用户引入了与程序分析算法交互的新界面，表明偏好，并提供对地面事实的反馈。对于分析用户，项目构建新的bug查找工具，为他们的程序提供有用的、可操作的洞察。对于分析设计者来说，这个项目提供了在程序验证中应用统计技术的新方法，以及产生精确的和可扩展的程序分析系统的新机会。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This award is funded in whole or in part under the American Rescue Plan Act of 2021 (Public Law 117-2).Program analysis and verification systems are both challenging to design and expensive to operate, with a reputation for poor scalability, false warnings, and missed bugs. In addition, these program-reasoning tools interoperate poorly with the continuous and iterative nature of modern software engineering processes, and only have rudimentary ways of interacting with human engineers. The project develops techniques to extend the underlying deductive basis of these analyses---commonly expressed using declarative formalisms such as constrained Horn clauses (CHCs) or Datalog---with probabilistic modes of reasoning. These probabilistic models provide a mechanism to prioritize warnings, incorporate feedback from developers, and combine knowledge from multiple analysis tools. As such, the project's main impact is to significantly improve the accuracy and usability of program analysis technology.The project develops algorithms to automatically learn probabilistic models from analysis of implementations, and determine their accuracy using open-source code corpora such as GitHub and databases such as Common Vulnerabilities and Exposures (CVE). Next, it develops ranking techniques to optimize effective accuracy, time needed to discover bugs, and other programmer-specified relevance criteria. The project introduces new interfaces for users to interact with program analysis algorithms, indicate preferences, and provide feedback on ground truth. For the analysis user, the project builds new bug-finding tools that provide useful, actionable insight into their programs. For analysis designers, the project offers new ways to apply statistical techniques in program verification, and new opportunities to produce accurate and scalable program analysis systems.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.