Content area
Randomized algorithms are hard to test, thus accentuating the need for formal methods to ensure their correctness. When probabilistic separation logic was first developed as a formal method for proving probabilistic independence between program variables, it was unclear whether this approach generalizes to weaker forms of probabilistic separation used in program analysis.
We first overview existing work in Bunched logic — the assertion logic underlying separation logic — and probabilistic separation logic for independence in chapter 2.
In chapter 3, we extend probabilistic separation logic to reason about negative dependence, a relation in which an increase in one variable makes others less likely to increase. We demonstrate the utility of this program logic by analyzing hash-based data structures, such as Bloom filters.
In chapter 4, we introduce a variation of probabilistic separation logic for reasoning about dependence and independence. Specifically, we use it to establish conditional independence between programs variables in simple programs.
Last, in chapter 5, we present the unary fragment of BLUEBELL to provide a more ergonomic way to reason about conditional independence and independence. We illustrate its application through more intricate examples drawn from cryptography, security, and probabilistic graphical models.
All the program logics developed in this thesis target imperative programs that can sample from probability distributions.
