**CAREER: SHF: Compositional Analysis of Randomized Algorithms** **NSF Award [ #1943130 ](https://www.nsf.gov/awardsearch/showAward?AWD_ID=1943130)** # Synopsis 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. # Personnel * [Justin Hsu](https://justinh.su) (PI) * [Jialu Bao](https://baojia.lu/about/) (PhD student) * [Zachary Susag](https://zacharysusag.net/) (PhD student) # Collaborators * Aws Albarghouthi (University of Wisconsin) * Gilles Barthe (MPI S&P) * Simon Docherty (Droit) * Marco Gaboardi (Boston University) * Benjamin Kaminski (University College London) * Joost-Pieter Katoen (RWTH Aachen) * Subhajit Roy (IIT Kanpur) * Alexandra Silva (Cornell) * Joseph Tassarotti (Boston College) * Mingsheng Ying (University of Technology Sydney) * Nengkun Yu (University of Technology Sydney) # Publications 1. Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. A Bunched Logic for Conditional Independence. LICS 2021. [[paper](https://arxiv.org/abs/2008.09231)] 2. Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. LICS 2021. [[paper](https://arxiv.org/abs/2102.00329)] 3. Subhajit Roy, Justin Hsu, and Aws Albarghouthi. Learning Differentially Private Mechanisms. IEEE S&P 2021. [[paper](https://arxiv.org/abs/2101.00961)] 4. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. A Pre-Expectation Calculus for Probabilistic Sensitivity. POPL 2021. **Distinguished Paper Award**. [[paper](https://arxiv.org/abs/1901.06540)] [[blog](https://blog.sigplan.org/2021/07/15/a-pre-expectation-calculus-for-probabilistic-sensitivity/)] 5. Gilles Barthe, Justin Hsu, and Kevin Liao. A Probabilistic Separation Logic. POPL 2020. [[paper](https://arxiv.org/abs/1907.10708)] 6. Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. A Separation Logic for Negative Dependence. POPL 2022. [[paper](https://arxiv.org/abs/2111.14917)] 7. Karuna Grewal, Loris D’Antoni, and Justin Hsu. P4BID: Information Flow Control in P4. PLDI 2022. [[paper](https://arxiv.org/abs/2204.03113)] 8. Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. Data-Driven Invariant Learning for Probabilistic Programs. CAV 2022. **Distinguished Paper Award.** [[paper](https://arxiv.org/abs/2106.05421)] 9. Zachary Susag, Sumit Lahiri, Justin Hsu, and Subhajit Roy. Symbolic Execution for Randomized Programs. OOPSLA 2022. [[paper](https://arxiv.org/abs/2209.08046)] # Code * Exist: Data-Driven Invariant Learning for Probabilistic Programs. Code for CAV 2022 paper. [code](https://github.com/JialuJialu/Exist) * Plinko: Symbolic Execution for Randomized Programs. Code for OOPSLA 2022 paper. [code](https://doi.org/10.48550/arXiv.2209.08046) # Education * CS 538: Introduction to the Theory and Design of Programming Languages (University of Wisconsin) [[materials](https://justinh.su/teaching/s20/cs538/)] [[blog](https://blog.sigplan.org/2021/01/28/re-imagining-the-programming-paradigms-course/)] * CS 763: Security and Privacy in Data Science (University of Wisconsin) [[materials](https://justinh.su/teaching/f20/cs763/)] * Invited course: Reasoning about Probabilistic Programs ([OPLSS 2021](https://www.cs.uoregon.edu/research/summerschool/summer21/index.php)) [[slides](https://justinh.su/files/slides/oplss21.pdf)] [[recordings](https://www.cs.uoregon.edu/research/summerschool/summer21/topics.php)] * CS 6182: Foundations of Probabilistic Programming (Cornell University) [[materials](https://www.cs.cornell.edu/courses/cs6182/2021fa//)] * CS 6117: Category Theory for Computer Scientists (Cornell University) [[materials](https://www.cs.cornell.edu/courses/cs6117/2022fa/)] [[blog](https://blog.sigplan.org/2023/04/04/teaching-category-theory-to-computer-scientists/)] # Outreach * Programming Languages Mentoring Workshop@POPL 2021 (Organizer) [[site](https://popl21.sigplan.org/home/PLMW-2021)] [[blog](https://blog.sigplan.org/2021/05/11/programming-languages-mentoring-workshop-ten-years-later/)] * Programming Languages Mentoring Workshop 2021-2023 (Steering Committee) * Conference on Mathematical Foundations of Programming Semantics (MFPS) 2022 (Co-Chair) * Cornell Bowers CIS Undergraduate Research Experience (Director) [[site](https://bure.cis.cornell.edu/)]