Reasoning about the effect of uncertainties on programs is a fundamental challenge in static analysis. A large volume of research has focused on numerical and symbolic abstract domains for reasoning about nondeterministic choices in programs. In this talk, we will explore recent results on proving properties of programs with probabilities. Such programs arise in a wide variety of applications ranging from data mining to cyber-physical systems. We examine how existing abstract domains can reason about such programs, and present recent work that considers the combination of abstract domain reasoning with results from martingale theory and concentration of measure inequalities. We conclude with an examination of open challenges and future applications in this area.