Andrew C. Myers

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

This work introduces Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary that models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary...