Verifying probabilistic programs using a Hoare like logic

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

    7 Citations (Scopus)

    Abstract

    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
    PublisherSpringer
    Pages790-
    ISBN (Print)3-540-66856-X
    DOIs
    Publication statusPublished - 1999

    Publication series

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

    Fingerprint

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

    Cite this