mwang@watmath.UUCP (mwang) (07/18/83)
_D_E_P_A_R_T_M_E_N_T _O_F _C_O_M_P_U_T_E_R _S_C_I_E_N_C_E
_U_N_I_V_E_R_S_I_T_Y _O_F _W_A_T_E_R_L_O_O
_S_E_M_I_N_A_R _A_C_T_I_V_I_T_I_E_S
_T_H_E_O_R_Y _S_E_M_I_N_A_R
- Thursday, July 21, 1983.
Dr. Dexter Kozen of IBM Research Center, Yorktown
Heights, will speak on ``Probabilistic Program Verifi-
cation''.
TIME: 3.30 PM
ROOM: MC 5158
ABSTRACT
This talk concerns a probabilistic analog PPDL of Pro-
positional Dynamic Logic. PPDL is useful in the formal
manipulation of simple probabilistic programs and
average-case analysis of deterministic programs. In
this talk we describe the system and its deductive cal-
culus, and illustrate its use by calculating the ex-
pected running time of a simple random walk. We also
describe briefly a polynomial- space decision procedure
for deciding the truth of formulas involving well-
structured programs.
July 18, 1983