How Often Does Your Program Fail?

RESUMO

Software in production encounters inputs shaped by how it is used in practice. We study distribution-aware reliability estimation: given a program, its operational input distribution, and a condition of interest, determine how often that condition holds and certify the result with a guaranteed error bound. Symbolic and statistical methods offer two ways to answer this question. Symbolic methods reason about entire regions of the input space and can certify rates exactly, but often struggle with complex arithmetic or loops. Statistical methods instead sample inputs and apply concentration bounds. They are broadly applicable, but can require many samples when failures are rare. We bring these approaches together in a framework that includes both as special cases. Each estimator has three components: a mass estimator, a per-leaf confidence bound, and a symbolic closure rule. We prove that any instantiation satisfying three invariants returns an interval containing the true rate with confidence 1-delta, regardless of when it stops. The certified error has two parts: a statistical term, reduced by sampling, and a structural term, reduced by symbolic closure. Pure sampling and pure symbolic execution each reduce only one of these terms. Alternative choices of the components also allow the framework to support rare-event variance-reduction methods.