Reasoning about Recursive Probabilistic Programs

DOI10.1145/2933575.2935317zbMath1401.68048arXiv1603.02922OpenAlexW2294463722MaRDI QIDQ4635928

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

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

Related Items (8)

Formal semantics of a classical-quantum language ⋮ A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Calibrating generative models: the probabilistic Chomsky-Schützenberger hierarchy ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ A Type Theory for Probabilistic and Bayesian Reasoning ⋮ Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes

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