Proving programs robust

Abstract

We present a program analysis for verifying quantitative robustness properties of programs, stated generally as: "If the inputs of a program are perturbed by an arbitrary amount epsilon, then its outputs change at most by (K . epsilon), where K can depend on the size of the input but not its value." Robustness properties generalize the analytic notion of continuity---e.g., while the function ex is continuous, it is not robust. Our problem is to verify the robustness of a function P that is coded as an imperative program, and can use diverse data types and features such as branches and loops.