Formalising Semantics for Expected Running Time of Probabilistic Programs
DOI10.1007/978-3-319-43144-4_30zbMATH Open1478.68138OpenAlexW2494065672MaRDI QIDQ2829281FDOQ2829281
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
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
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)
Cites Work
- Abstraction, Refinement and Proof for Probabilistic Systems
- Proofs of randomized algorithms in Coq
- Title not available (Why is that?)
- Probabilistic guarded commands mechanized in HOL
- Probabilistic functions and cryptographic oracles in higher order logic
- 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
- Title not available (Why is that?)
- Verified analysis of random binary tree structures
- Markov chains and Markov decision processes in Isabelle/HOL
Uses Software
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)
