Jialu Bao

Jialu Bao

About me

I am a postdoctoral researcher at Northeastern University, working with Prof. Steven Holtzen. I received my Ph.D. from Cornell University, advised by Prof. Justin Hsu.

I develop formal methods to specify and verify the correctness of programs. One focus of my research is verifying probabilistic programs. They power applications such as cryptographic protocols and differential privacy, yet their randomness makes correctness and performance notoriously hard to test or reason about. I design probabilistic separation logics that exploit probabilistic independence, conditional independence, and negative dependence to enable compositional proofs about such programs. I also work on automating probabilistic separation logic and other deductive verification methods, with the goal of making these formal methods more accessible.

Beyond probabilistic program verification, I am also interested in:

  • a cleaner characterization of causal inference and its automation;
  • formal verification of consensus protocols.

During my PhD, I also enjoyed organizing Cornell’s Programming Language Discussion Group (PLDG) and volunteering for the SIGPLAN’s long-term mentoring program for a few years.

Email: jialu8ao@gmail.com

Thesis

Probabilistic Separation Logics for Randomized Algorithms
Jialu Bao.
[PDF]

Publications

Towards an Equational Calculus of Interventions
Shubh Agrawal, Jialu Bao, Steven Holtzen.
The Languages for Inference Workshop (LAFI) 2026.
[extended abstract]

Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Jialu Bao, Emanuele D’Osualdo, Azadeh Farzan.
Symposium on Principles of Programming Languages (POPL) 2025.
[arxiv] [20-min talk] [doi]

A Categorical Approach to DIBI Models
Tao Gu, Jialu Bao, Justin Hsu, Alexandra Silva, and Fabio Zanasi.
Formal Structures for Computation and Deduction (FSCD) 2024.
[arxiv] [doi]

Mixture Languages
Oliver Richardson, Jialu Bao.
The Languages for Inference Workshop (LAFI) 2024.
[extended abstract]

Data-Driven Invariant Learning for Probabilistic Programs
Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, Subhajit Roy.
Distinguished Paper Award, Computer Aided Verification (CAV) 2022.
Journal version appears on Formal Methods in Systems Design (FMSD) 2025.
[arxiv] [extended abstract] [slide] [doi]

A Separation Logic for Negative Dependence
Jialu Bao, Marco Gaboardi, Justin Hsu, Joseph Tassarotti.
Symposium on Principles of Programming Languages (POPL) 2022.
[arxiv] [5 min video] [20 min video] [doi]

A Bunched Logic for Conditional Independence
Jialu Bao, Simon Docherty, Justin Hsu, Alexandra Silva.
Symposium on Logic in Computer Science (LICS) 2021.
[arxiv] [video] [doi]

Hidden Community Detection on Two-layer Stochastic Models Theoretical Prospective
Jialu Bao, Kun He, Xiaodong Xin, Bart Selman, John E. Hopcroft.
Theory and Applications of Models of Computation (TAMC) 2020.
Journal version appears on Transactions on Knowledge Discovery from Data (TKDD) 2025.
[TAMC arxiv] [TKDD arxiv] [doi]

News

  • 2025.7 I passed my B exam (thesis defense)!
  • 2025.3 - 2025.5 I had the pleasure of visiting Prof. Alexandra Silva’s group at University College London!
  • 2024.5 - 2025.8 I had the opportunity to intern with a wonderful team at Basis Research Institute!
Show older newsHide older news
  • 2024.1 - 2024.5 I co-organized a new edition of the Great Works in PL Seminar with Yulun Yao!
  • 2023.8 I attended Marktoberdorf Summer School.
  • 2023.3 I was humbled to receive an honorable mention for the Jane Street Graduate Research Fellowship.
  • 2022.8 I joined the Operations Team of SIGPLAN Long-Term Mentoring Committee! The program welcomes aspiring and current programming languages researchers from all walks of life to serve as mentors, mentees, or both. SIGPLAN members and non-members alike are welcome, and there is no cost to participate. There are no limitations on country of residence or languages spoken.
  • 2022.8 I passed my A exam and became a Ph.D. candidate.
  • 2022.7 I attended the Oregon Programming Languages Summer School (OPLSS) .

Talks

Automating Probabilistic Separation Logic [slide]
Software Day, Northeastern University · March 2026.

Automating Probabilistic Separation Logic
Upstate PL Seminar y · August 2025.

Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning
PLV Seminar, Portland State University · March 2025.

Bluebell: An Alliance of Relational Lifting and Independence for Probabilistic Reasoning [slide]
PLDG, Cornell University · October 2024.

A Tour of Probabilistic Separation Logic [slide]
Basis Research Institute · August 2024.

A Separation Logic for Negative Dependence
POPV Seminar, Boston University · November 2023.

Data-Driven Invariant Learning for Probabilistic Programs
OPLSS 2022 Participants’ Talks · June 2022.

Data-Driven Invariant Learning for Probabilistic Programs [slides]
PLDG, Cornell University · March 2022.

A Separation Logic for Negative Dependence [slides]
PLDG, Cornell University · October 2021.

Data-Driven Invariant Learning for Probabilistic Programs (preliminary work)
PPS-PIHOC-DIAPASoN Workshop · February 2021.

A Logic for Verifying Conditional Independence and Join Dependency (poster)
Student Research Competition, POPL 2020 · January 2020.

Teaching