Incorporating assertions into code is a powerful way to increase confidence in correctness with greater precision than testing. Unfortunately, the ideal assertions often require deep traversal of a large object graph or expensive computation of a quantified formula. Because of this run-time cost, usage of assertions is typically confined to testing environments and disabled in production environments. The spectrum of input data against which code is run in production dwarfs testing environments, so production-disabled assertions sacrifice significant potential robustness. This work presents a new middle ground between expensive “always-on” behavior and unsound ``always-off'' behavior for run-time assertions, by gradually transitioning from “on” to “off” as confidence in code correctness increases over time. A novel static analysis determines the exact extent to which each assertion depends on its surrounding code under a probabilistic model of program execution, allowing demonstration that even as the frequency of assertion execution decreases, confidence in correctness does not. This system combines the robustness of “always-on” assertions with the scalability and eventually zero overhead of “always-off” assertions, providing a powerful new sweet spot in design of testing and correctness systems.

Research Advisor: Andrew Myers ACM member number: 3741362 Category: PhD student