CAREER: SHF: Compositional Analysis of Randomized Algorithms

CAREER: SHF: Compositional Analysis of Randomized Algorithms
NSF Award #2153916
Synopsis · Personnel · Collaborators · Publications · Code · Education · Outreach

   

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

   

Collaborators

   

Publications

  1. Jialu Bao, Simon Docherty, Justin Hsu, and Alexandra Silva. A Bunched Logic for Conditional Independence. LICS 2021. [paper]
  2. Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. LICS 2021. [paper]
  3. Subhajit Roy, Justin Hsu, and Aws Albarghouthi. Learning Differentially Private Mechanisms. IEEE S&P 2021. [paper]
  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] [blog]
  5. Gilles Barthe, Justin Hsu, and Kevin Liao. A Probabilistic Separation Logic. POPL 2020. [paper]
  6. Jialu Bao, Marco Gaboardi, Justin Hsu, and Joseph Tassarotti. A Separation Logic for Negative Dependence. POPL 2022. [paper]
  7. Karuna Grewal, Loris D’Antoni, and Justin Hsu. P4BID: Information Flow Control in P4. PLDI 2022. [paper]
  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]
  9. Zachary Susag, Sumit Lahiri, Justin Hsu, and Subhajit Roy. Symbolic Execution for Randomized Programs. OOPSLA 2022. [paper]
  10. Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi. A Categorical Approach to DIBI Models. FSCD 2024. [paper]
  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]
  12. Ariel E. Kellison and Justin Hsu. Numerical Fuzz: A Type System for Rounding Error Analysis. PLDI 2024. [paper]
  13. Jialu Bao, Emanuele D'Osualdo, and Azadeh Farzan. Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning. POPL 2025. [paper]

   

Code

   

Education

   

Outreach

formatted by Markdeep 1.18  
✒