Unified Analysis Techniques for Programs with Outcomes

The theories required for program analysis have evolved past the foundations developed decades ago. Programs display computational effects such as nondeterminism, randomization, exceptions, and mutable state. Orthogonally, bug-finding is often more tangible than establishing correctness. Specialized techniques have been introduced to handle effects and incorrectness reasoning. While successful, the disjointed nature of those techniques means that new analysis systems must be built to analyze each kind of program and property. In my research, I am creating a logical foundation to consolidate the aforementioned theories, with which I plan to develop a new generation of static analysis tools that are simpler and more efficient than those available today.