The enormous rise in the scale, scope, and complexity of software projects has created a thriving marketplace for program analysis and verification tools. Despite routine adoption by industry, developing such tools remains challenging, and their designers must carefully balance tradeoffs between false alarms, missed bugs, and scalability to large codebases. Furthermore, when tools fail to verify some program property, they only provide coarse estimates of alarm relevance, potential severity, and of the likelihood of being a real bug, thereby limiting their usefulness in software projects with large teams.

I will present a framework that extends contemporary program reasoning systems with rich probabilistic models. These models emerge naturally from the program structure, and probabilistic inference refines the deductive process of the underlying system. In experiments with large programs, such probabilistic graphical representations of program structure enable an order-of-magnitude reduction in false alarm rates and invocations of expensive reasoning engines such as SMT solvers.

To the analysis user, these techniques offer a lens by which to focus their attention on the most important alarms and a uniform method for the tool to interactively generalize from human feedback. To the analysis designer, they offer novel opportunities to leverage data-driven approaches in analysis design. And to researchers, they offer new challenges while performing inference in models of unprecedented size.