Andrew C. Myers

Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reas...