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…