Verification of Probabilistic Programs
Micha Sharir, Amir Pnueli and Sergiu Hart
Abstract
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
-
SIAM Journal on Computing
13 (1984), 2, 292-314
Related papers on probabilistic programs by S. Hart, A. Pnueli and M.
Sharir: