Coupling proofs are probabilistic product programs

DOI10.1145/3009837.3009896zbMath1380.68267arXiv1607.03455OpenAlexW3100368036MaRDI QIDQ5370853

Pierre-Yves Strub, Justin Hsu, Gilles Barthe, Benjamin Grégoire

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

probabilistic algorithmsformal verificationprobabilistic couplingsrelational Hoare logicproduct programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

CryptHOL: game-based proofs in higher-order logic ⋮ Divergences on monads for relational program logics ⋮ Foundations for entailment checking in quantitative separation logic ⋮ Generating functions for probabilistic programs

This page was built for publication: Coupling proofs are probabilistic product programs