Verifying probabilistic programs using a hoare like logic


Hartog, J.I. den and Vink, E.P. de (2002) Verifying probabilistic programs using a hoare like logic. International journal of foundations of computer science, 13 (3). pp. 315-340. ISSN 0129-0541

[img] PDF
Restricted to UT campus only
: Request a copy
PDF (Author's version)
Abstract:Probability, be it inherent or explicitly introduced, has become an important issue in the verification of programs. In this paper we study a formalism which allows reasoning about programs which can act probabilistically. To describe probabilistic programs, a basic programming language with an operator for probabilistic choice is introduced and a denotational semantics is given for this language. To specify propertics of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates is introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be sound and complete; the properties that can be derived are exactly the valid properties. Finally some typical examples illustrate the use of the probabilistic predicates and the proof system.
Item Type:Article
Copyright:© 2002 World Scientific
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page