Verifying probabilistic programs using a Hoare like logic

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    10 Citaten (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.
    Originele taal-2Engels
    TitelAdvances in Computing Science - ASIAN'99 (Proceedings 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999)
    RedacteurenP.S. Thiagarajan, R. Yap
    ISBN van geprinte versie3-540-66856-X
    StatusGepubliceerd - 1999

    Publicatie series

    NaamLecture Notes in Computer Science
    ISSN van geprinte versie0302-9743


    Duik in de onderzoeksthema's van 'Verifying probabilistic programs using a Hoare like logic'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit