Verifying Probabilistic Programs Using a Hoare like Logic

J.I. den Hartog, E.P. De Vink

    Research output: Contribution to journalArticleAcademicpeer-review

    33 Citations (Scopus)
    410 Downloads (Pure)

    Abstract

    Probability, be it inherent or explicitly introduced, has become an important issue in the verification of many programs. 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 properties of probabilistic programs, standard first order logic predicates are insufficient, so a notion of probabilistic predicates are introduced. A Hoare-style proof system to check properties of probabilistic programs is given. The proof system for a sublanguage is shown to be correct 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.
    Original languageEnglish
    Pages (from-to)315-340
    JournalInternational journal of foundations of computer science
    Volume13
    Issue number3
    DOIs
    Publication statusPublished - Jun 2002

    Keywords

    • IR-55799
    • EWI-882

    Fingerprint

    Dive into the research topics of 'Verifying Probabilistic Programs Using a Hoare like Logic'. Together they form a unique fingerprint.

    Cite this