38 citations · 59 across the 7 of their papers we have counts for
8 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…
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…
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…
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski +1
We present a novel \emph{weakest pre calculus} for \emph{reasoning about quantitative hyperproperties} over \emph{nondeterministic and probabilistic} programs. Whereas existing cal…
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…
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
Noam Zilberstein, Angelina Saliling, Alexandra Silva
Separation logic's compositionality and local reasoning properties have led to significant advances in scalable static analysis. But program analysis has new challenges -- many pro…
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
Noam Zilberstein, Derek Dreyer, Alexandra Silva
Program logics for bug-finding (such as the recently introduced Incorrectness Logic) have framed correctness and incorrectness as dual concepts requiring different logical foundati…