2023
Data-Driven Invariant Learning for Probabilistic Programs (Extended Abstract)
IJCAI 2023poster
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…