Reasoning about Recursive Probabilistic Programs

DOI10.1145/2933575.2935317MaRDI QIDQ4635928zbMATH OpenOpenAlexFDO

Authors Federico Olmedo, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.02922

zbMATH Keywords

recursionprogram verificationexpected runtimeprobabilisitic programmingweakest pre-condition calculus

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Reasoning about probabilistic sequential programs
• Reasoning about probabilistic sequential programs in a probabilistic logic
• scientific article; zbMATH DE number 3890702
• Reasoning About States of Probabilistic Sequential Programs
• Automated reasoning for probabilistic sequential programs with theorem proving
• Mathematics of Program Construction
• Understanding probabilistic programs
• Fine-grained semantics for probabilistic programs
• Probabilistic programming inference via intensional semantics

Cited in

(24)

• Runtime analysis of probabilistic programs with unbounded recursion
• Calibrating generative models: the probabilistic Chomsky-Schützenberger hierarchy
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Time-bounded termination analysis for probabilistic programs with delays
• Weakest precondition reasoning for expected run-times of probabilistic programs
• A weakest pre-expectation semantics for mixed-sign expectations
• Probabilistic programming inference via intensional semantics
• Efficient analysis of probabilistic programs with an unbounded counter
• Reasoning about probabilistic sequential programs
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• On Lexicographic Proof Rules for Probabilistic Termination
• A type theory for probabilistic and Bayesian reasoning
• On lexicographic proof rules for probabilistic termination
• Runtime analysis of probabilistic programs with unbounded recursion
• scientific article; zbMATH DE number 1692951 (Why is no real title available?)
• Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
• Refinement algebra for probabilistic programs
• Quantum weakest preconditions for reasoning about expected runtimes of quantum programs
• A denotational semantics for low-level probabilistic programs with nondeterminism
• Formal semantics of a classical-quantum language
• Inferring covariances for probabilistic programs
• scientific article; zbMATH DE number 3890702 (Why is no real title available?)
• Certificates for probabilistic pushdown automata via optimistic value iteration

This page was built for publication: Reasoning about Recursive Probabilistic Programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635928)