Jialu Bao

Data-Driven Invariant Learning for Probabilistic Programs (Extended Abstract)

The weakest pre-expectation framework from Morgan and McIver for deductive verification of probabilistic programs generalizes binary state assertions to real-valued expectations to measure expected values of expressions over probabilistic program variables. While loop-free programs can be analyzed b…