CAREER: Foundations of Statistical Program Reasoning

职业：统计程序推理的基础

• 批准号: 2146518
• 负责人: Mukund Raghothaman
• 金额: $ 64万
• 依托单位: University of Southern California
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-02-01 至 2027-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2146518&HistoricalAwards=false
• 关键词: CAREER; Foundations; Statistical; Program; Reasoning

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.

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

项目成果

Learning probabilistic models for static analysis alarms

学习静态分析警报的概率模型

• DOI: 10.1145/3510003.3510098
• 发表时间: 2022
• 期刊: International Conference on Software Engineering
• 作者: Kim, Hyunsu;Raghothaman, Mukund;Heo, Kihong
• 通讯作者: Heo, Kihong