Formalising Semantics for Expected Running Time of Probabilistic Programs

DOI10.1007/978-3-319-43144-4_30MaRDI QIDQ2829281zbMATH OpenOpenAlexFDO

Authors Johannes Hölzl

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_30

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Computing expected runtimes for constant probability programs
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Fine-grained semantics for probabilistic programs
• Probabilistic semantics and program analysis
• Probabilistic semantics of terminating programs
• scientific article; zbMATH DE number 4076588
• Reasoning about probabilistic sequential programs
• Runtime analysis of probabilistic programs with unbounded recursion
• Runtime analysis of probabilistic programs with unbounded recursion
• Application ofComputable Distributions to the Semantics of Probabilistic Programs

Cites work

• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• Abstraction, Refinement and Proof for Probabilistic Systems
• Probabilistic functions and cryptographic oracles in higher order logic
• Probabilistic guarded commands mechanized in HOL
• Proofs of randomized algorithms in Coq
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited in

(6)

• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Weakest precondition reasoning for expected runtimes of randomized algorithms
• scientific article; zbMATH DE number 2147036 (Why is no real title available?)
• Verified analysis of random binary tree structures
• Markov chains and Markov decision processes in Isabelle/HOL

Describes a project that uses

Uses Software

• Markov Models
• pGCL
• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Formalising Semantics for Expected Running Time of Probabilistic Programs

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