Static Analysis of Programs with Imprecise Probabilistic Inputs

Abstract. Having a precise yet sound abstraction of the inputs of nu-merical programs is important to analyze their behavior. For many pro-grams, these inputs are probabilistic, but the actual distribution used is only partially known. We present a static analysis framework for rea-soning about programs with inputs given as imprecise probabilities: we define a collecting semantics based on the notion of previsions and an ab-stract semantics based on an extension of Dempster-Shafer structures. We prove the correctness of our approach and show on some realistic examples the kind of invariants we are able to infer.