Jialu Bao

Jialu Bao

My first name is pronounced as J·ah·loo.

About me

I am a computer science Ph.D. student at Cornell, working on the verification of randomized algorithms. The correctness and performance of randomized algorithms are often difficult to test or reason about. I want to address this problem by enabling simple and compositional formal proofs of probabilistic programs. I am very fortunate to be advised by Prof. Justin Hsu to explore my interests.

Before moving to Cornell with my advisor, I spent two wonderful years at University of Wisconsin – Madison as a Ph.D. student, and prior to that, I did my undergrad also at Cornell majoring in Mathematics and Computer Science.

Email: jb965@cornell.edu

Publications

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]

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

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 will appear on Formal Methods in Systems Design (FMSD).
[arxiv] [extended abstract] [slide]

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]

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

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 will appear on Transactions on Knowledge Discovery from Data (TKDD).
[conference version arxiv] [journal version arxiv]

News

Talks

  • 2024.10 Talked about “Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning” at Cornell’s PLDG.

  • 2024.02 Presented “Views: Compositional Reasoning for Concurrent Programs” by Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson and Hongseok Yang at Cornell’s PLDG.

  • 2023.11 Talked about “A Separation Logic for Negative Dependence” at Boston University’s POPV seminar.

  • 2023.03 Presented “Proving Hypersafety Compositionally” by Emanuele D’Osualdo, Azadeh Farzan and Derek Dreyer at Cornell’s PLDG. (slide)

  • 2022.09 Led discussion of Impossibility of Distributed Consensus with One Faulty Process (the seminal FLP impossibility result) in CS 6410 Advanced Systems. (slide)

  • 2022.08 Proposed “Formally Reasoning about (In)dependencies in Probabilistic Programs” for my A-Exam. (slide)

  • 2022.06 Presented “Data-Driven Invariant Learning for Probabilistic Programs” at OPLSS 2022 Participants Talk.

  • 2022.03 Presented “Data-Driven Invariant Learning for Probabilistic Programs” at Cornell’s PLDG. (slide)

  • 2022.02 Led discussion of “Sometimes” and “not never” revisited: on branching versus linear time temporal logic at Cornell PL’s Great Works seminar. (slide)

  • 2021.10 Presented “A Separation Logic for Negative Dependence” at Cornell’s PLDG. (slide)

  • 2021.02 Presented a preliminary work on “Data-Driven Invariant Learning for Probabilistic Programs” at PPS-PIHOC-DIAPASoN Workshop!

  • 2020.10 Led discussion of Data-Driven Inference of Representation Invariants by Anders Miltner, Saswat Padhi, Todd Millstein and David Walker at UW Madison’s PL seminar.

  • 2020.01 Presented a poster on “A Logic for Verifying Conditional Independence and Join Dependency” at POPL 2020’s Student Research Competition.

Teaching