4 papers
Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary
Hanxi Chen, Noam Zilberstein, Andrew C. Myers +1
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…
Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
Noam Zilberstein, Alexandra Silva, Joseph Tassarotti
Although randomization has long been used in distributed computing, formal methods for reasoning about probabilistic concurrent programs have lagged behind. No existing program log…
Total Outcome Logic: Unified Reasoning for a Taxonomy of Program Logics
James Li, Noam Zilberstein, Alexandra Silva
While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includ…
A Demonic Outcome Logic for Randomized Nondeterminism
Noam Zilberstein, Dexter Kozen, Alexandra Silva +1
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but the…