### Abstract

Original language | Undefined |
---|---|

Pages | 113-125 |

Number of pages | 13 |

DOIs | |

State | Published - Dec 1999 |

### Fingerprint

### Keywords

- IR-56196
- EWI-1035

### Cite this

*Verifying Probabilistic Programs Using a Hoare like Logic*. 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).

Research output: Scientific - peer-review › Paper

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 -