Verifying probabilistic programs using a Hoare like logic

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    10 Citations (Scopus)


    Hoare logic can be used to verify properties of deterministic programs by deriving correctness formulae, also called Hoare triples. The goal of this paper is to extend the Hoare logic to be able to deal with probabilistic programs. To this end a generic non-uniform language Lpw with a probabilistic choice operator is introduced and a denotational semantics D is given for the language. A notion of probabilistic predicate is defined to express claims about the state of a probabilistic program. To reason about the probabilistic predicates a derivation system pH, similar to that of standard Hoare logic, is given. The derivation system is shown to be correct with respect to the semantics D. Some basic examples illustrate the use of the system.
    Original languageEnglish
    Title of host publicationAdvances in Computing Science - ASIAN'99 (Proceedings 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999)
    EditorsP.S. Thiagarajan, R. Yap
    ISBN (Print)3-540-66856-X
    Publication statusPublished - 1999

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Dive into the research topics of 'Verifying probabilistic programs using a Hoare like logic'. Together they form a unique fingerprint.

    Cite this