Verification of Probabilistic Programs

Micha Sharir, Amir Pnueli and Sergiu Hart

(Acrobat PDF file)


A general method for proving properties of probabilistic programs is presented. This method generalizes the intermediate assertion method in that it extends a given assertion on the output distribution into an invariant assertion on all intermediate distributions, too. The proof method is shown to be sound and complete for programs which terminate with probability 1. A dual approach, based on the expected number of visits in each intermediate state, is also presented. All the methods are presented under the uniform framework which considers a probabilistic program as a discrete Markov process.

Key words. program verification, probabilistic programs, Markov chains

CR categories. 5.24, 5.5

Related papers on probabilistic programs by S. Hart, A. Pnueli and M. Sharir: