Proving uniformity and independence by self-composition and coupling

DOI10.29007/vz48zbMath1403.68140arXiv1701.06477OpenAlexW2950053966MaRDI QIDQ4645748

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

Publication date: 10 January 2019

Published in: EPiC Series in Computing (Search for Journal in Brave)

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

zbMATH Keywords

independenceuniformityprogram verificationrelational logicprobabilistic programs

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Uses Software

• EasyCrypt