Randomized algorithms are hard to test, thus accentuating the need for formalmethods to ensure their correctness. When probabilistic separation logic was first developed as a formal method for proving probabilistic independence be- tween 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 negativedependence, 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 forreasoning 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 amore 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 programsthat can sample from probability distributions.