CAREER: SHF: Compositional Analysis of Randomized Algorithms

职业：SHF：随机算法的成分分析

• 批准号: 2153916
• 负责人: Justin Hsu
• 金额: $ 70.31万
• 依托单位: Cornell University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-01-01 至 2025-11-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2153916&HistoricalAwards=false
• 关键词: CAREER; SHF; Compositional; Analysis; Randomized

Randomized algorithms play a central role in important applications, including machine learning, data privacy, and cryptography. Like all software, probabilistic programs are susceptible to bugs. Furthermore, correctness properties rest on mathematical proof; missteps in these arguments can render algorithms incorrect before they are even implemented. Regardless of their source, errors may go unnoticed for years, posing increasing risks as probabilistic programs see broader adoption. This proposal seeks to advance the theory and practice of verification for probabilistic programs, developing technology to increase our confidence that these programs are correct. This project develops a software system to formally verify randomized algorithms, by leveraging three complementary ideas: (1) Employ higher-level properties that allows formal proofs to cover more ground with each step; (2) Strive for compositional reasoning which can allow complex systems to be verified by analyzing each component separately; and (3) Formalize human proof techniques which should inform verification methods. In the near term, results will enable verification for new algorithms. In the long term, this proposal works towards a world where all randomized programs can be computer-checked for correctness prior to deployment.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.

随机算法在重要应用中发挥着核心作用，包括机器学习，数据隐私和密码学。像所有的软件一样，概率程序容易出现错误。此外，正确性属性依赖于数学证明;这些参数中的失误可能会在算法实现之前就导致算法不正确。无论其来源如何，错误可能会被忽视多年，随着概率程序的广泛采用，风险越来越大。该提案旨在推进概率程序验证的理论和实践，开发技术以增加我们对这些程序正确性的信心。该项目开发了一个软件系统来正式验证随机算法，通过利用三个互补的想法：（1）采用更高级别的属性，允许正式证明在每个步骤中覆盖更多的地面;（2）努力进行组合推理，可以通过单独分析每个组件来验证复杂的系统;（3）形式化人工证明技术，应该告知验证方法。在短期内，这些结果将使新算法的验证成为可能。从长远来看，这项提议将致力于建立一个所有随机程序在部署前都能通过计算机检查正确性的世界。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Symbolic execution for randomized programs

• DOI: 10.1145/3563344
• 发表时间: 2022-09
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Zachary J. Susag;Sumitra Lahiri;Justin Hsu;Subhajit Roy

Data-Driven Invariant Learning for Probabilistic Programs

• DOI: 10.1007/978-3-031-13185-1_3
• 发表时间: 2021-06
• 作者: Jialu Bao;Drashti Pathak;Justin Hsu;Subhajit Roy

P4BID: information flow control in p4

• DOI: 10.1145/3519939.3523717
• 发表时间: 2022-04
• 期刊: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
• 作者: Karuna Grewal;Loris D'antoni;Justin Hsu

A Separation Logic for Negative Dependence

• DOI: 10.1145/3498719
• 发表时间: 2022-01-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Bao，Jialu;Gaboardi，Marco;Tassarotti，Joseph
• 通讯作者: Tassarotti，Joseph