2 papers
cs.PL2025
Data-Driven Invariant Learning for Probabilistic Programs
Jialu Bao, Nitesh Trivedi, Drashti Pathak +2
Morgan and McIver's weakest pre-expectation framework is one of the most well-established methods for deductive verification of probabilistic programs. Roughly, the idea is to gene…
cs.LO2024
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Jialu Bao, Emanuele D'Osualdo, Azadeh Farzan
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-st…