On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop

Xin Sun, Xingchi Su, Xiaoning Bian +1

Probabilistic Hoare logic (PHL) is an extension of Hoare logic and is specifically useful in verifying randomized programs. It allows researchers to formally reason about the behav…