Verifying probabilistic programs using a hoare like logic

Share/Save/Bookmark

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
2MB
[img]
Preview
PDF (Author's version)
355kB
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/55799
Official URL:http://dx.doi.org/10.1142/S012905410200114X
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page