Reasoning about Recursive Probabilistic Programs

Benjamin Lucien Kaminski; Christoph Matheja; Federico Olmedo; Joost-Pieter Katoen

REVIEW

Reasoning about Recursive Probabilistic Programs

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1603.02922 v1 pith:WPVHZSSE submitted 2016-03-09 cs.LO

Reasoning about Recursive Probabilistic Programs

Federico Olmedo , Benjamin Lucien Kaminski , Joost-Pieter Katoen , Christoph Matheja This is my paper

classification cs.LO

keywords programsprobabilisticrecursiveboundscalculusexpectationsobtainingwp-style

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original abstract

This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one-- and two--sided bounds for such expectations, and show the soundness of our wp-calculus with respect to a probabilistic pushdown automaton semantics. We also give a wp-style calculus for obtaining bounds on the expected runtime of recursive programs that can be used to determine the (possibly infinite) time until termination of such programs.

Reasoning about Recursive Probabilistic Programs

discussion (0)