Verifying Probabilistic Programs Using a Hoare like Logic

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

    • 6 Citations

    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 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
    Pages113-125
    Number of pages13
    DOIs
    StatePublished - Dec 1999

    Fingerprint

    Semantics

    Keywords

    • IR-56196
    • EWI-1035

    Cite this

    den Hartog, J., Thiagarajan, P. S. (Ed.), & Yap, R. (Ed.) (1999). Verifying Probabilistic Programs Using a Hoare like Logic. 113-125. DOI: 10.1007/3-540-46674-6_11

    den Hartog, Jeremy; Thiagarajan, P.S. (Editor); Yap, R. (Editor) / Verifying Probabilistic Programs Using a Hoare like Logic.

    1999. 113-125.

    Research output: Scientific - peer-reviewPaper

    @misc{fcba8111be4046ad8e661329cceb94eb,
    title = "Verifying Probabilistic Programs Using a Hoare like Logic",
    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 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.",
    keywords = "IR-56196, EWI-1035",
    author = "{den Hartog}, Jeremy and P.S. Thiagarajan and R. Yap",
    note = "Imported from DIES",
    year = "1999",
    month = "12",
    doi = "10.1007/3-540-46674-6_11",
    pages = "113--125",

    }

    den Hartog, J, Thiagarajan, PS (ed.) & Yap, R (ed.) 1999, 'Verifying Probabilistic Programs Using a Hoare like Logic' pp. 113-125. DOI: 10.1007/3-540-46674-6_11

    Verifying Probabilistic Programs Using a Hoare like Logic. / den Hartog, Jeremy; Thiagarajan, P.S. (Editor); Yap, R. (Editor).

    1999. 113-125.

    Research output: Scientific - peer-reviewPaper

    TY - CONF

    T1 - Verifying Probabilistic Programs Using a Hoare like Logic

    AU - den Hartog,Jeremy

    A2 - Thiagarajan,P.S.

    A2 - Yap,R.

    N1 - Imported from DIES

    PY - 1999/12

    Y1 - 1999/12

    N2 - 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.

    AB - 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.

    KW - IR-56196

    KW - EWI-1035

    U2 - 10.1007/3-540-46674-6_11

    DO - 10.1007/3-540-46674-6_11

    M3 - Paper

    SP - 113

    EP - 125

    ER -

    den Hartog J, Thiagarajan PS, (ed.), Yap R, (ed.). Verifying Probabilistic Programs Using a Hoare like Logic. 1999. Available from, DOI: 10.1007/3-540-46674-6_11