Formalising Semantics for Expected Running Time of Probabilistic Programs

DOI10.1007/978-3-319-43144-4_30zbMath1478.68138OpenAlexW2494065672MaRDI QIDQ2829281

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

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

Related Items (2)

Markov chains and Markov decision processes in Isabelle/HOL ⋮ Verified analysis of random binary tree structures

Uses Software

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

Cites Work

• Proofs of randomized algorithms in Coq
• Probabilistic guarded commands mechanized in HOL
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
• Abstraction, Refinement and Proof for Probabilistic Systems
• Unnamed Item

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