Synthesizing Probabilistic Invariants via Doob's Decomposition

Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti +1

When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then…