<meta charset="utf-8">

      **CAREER: SHF: Compositional Analysis of Randomized Algorithms**
      **NSF Award [ #2153916 ](https://www.nsf.gov/awardsearch/showAward?AWD_ID=2153916)**

# 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)
* Azadeh Farzan (University of Toronto)
* Marco Gaboardi (Boston University)
* Tao Gu (University College London)
* Benjamin Kaminski (University College London)
* Ariel Kellison (Sandia National Laboratories)
* Joost-Pieter Katoen (RWTH Aachen)
* Emanuele D'Osualdo (University of Konstanz)
* Subhajit Roy (IIT Kanpur)
* Alexandra Silva (Cornell University)
* Joseph Tassarotti (Boston College)
* Mingsheng Ying (University of Technology Sydney)
* Nengkun Yu (University of Technology Sydney)
* Fabio Zanasi (University College London)

# 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)]
10. Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi. A
  Categorical Approach to DIBI Models. FSCD 2024. [[paper](https://arxiv.org/abs/2401.05842)]
11. Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy.
  Data-Driven Invariant Learning for Probabilistic Programs. Formal Methods in
  System Design (previously appeared at CAV 2022).
  [[paper](https://arxiv.org/abs/2106.05421)]
12. Ariel E. Kellison and Justin Hsu. Numerical Fuzz: A Type System for Rounding
  Error Analysis. PLDI 2024. [[paper](https://arxiv.org/abs/2405.04612)]
13. Jialu Bao, Emanuele D'Osualdo, and Azadeh Farzan. Bluebell: An Alliance of
  Relational Lifting and Independence For Probabilistic Reasoning. POPL 2025.
  [[paper](https://arxiv.org/abs/2402.18708)]

# 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)
* Numerical Fuzz: A Type System for Rounding Error Analysis. Code for PLDI 2024 paper. [code](https://github.com/Athena-Types/NumFuzz)

# 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 2023 (Director) [[site](https://bure.cis.cornell.edu/)]

<!-- Markdeep: -->
<style class="fallback">body{visibility:hidden;white-space:pre;font-family:monospace}</style>
<script>window.markdeepOptions = {tocStyle: 'short'};</script>
<script src="markdeep.min.js" charset="utf-8"></script>
<script src="https://morgan3d.github.io/markdeep/latest/markdeep.min.js" charset="utf-8"></script>
<script>window.alreadyProcessedMarkdeep||(document.body.style.visibility="visible")</script>