Verifying Probabilistic Programs Using a Hoare like Logic

Jeremy den Hartog, P.S. Thiagarajan (Editor), R. Yap (Editor)

    Research output: Contribution to conferencePaperpeer-review

    10 Citations (Scopus)
    2 Downloads (Pure)


    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 L_pw 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 languageUndefined
    Number of pages13
    Publication statusPublished - Dec 1999
    Event5th Asian Conference on Advances in Computing Science, ASIAN 1999 - Phuket, Thailand
    Duration: 10 Dec 199912 Dec 1999


    Conference5th Asian Conference on Advances in Computing Science, ASIAN 1999
    OtherDecember 10-12, 1999


    • IR-56196
    • EWI-1035

    Cite this