Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proceedings of the ACM on Programming Languages, 5(POPL):1-30, 2021. [doi]
Abstract is missing.