5 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…
Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
Noam Zilberstein
Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning a…
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…