Abstract

ion is a fundamental tool for reasoning about a complex system. Program abstraction has been utilized to great effect for analyzing deterministic programs. At the heart of a program abstraction is a connection between the abstract program, which is simple to analyze, and the concrete program, which may be extremely complex. Program abstractions, however, are typically not probabilistic. In this thesis I generalize a particular class of non- deterministic program abstractions known as sound over-approximations to the probabilistic context. Sound over-approximations are a family of abstract programs which are guaranteed to contain the original program as a subset of their behavior. This thesis shows that when imbued with a probabilistic semantics, sound over-approximations define a family of probabilistic programs which capture key properties of the original program. It then introduces a mechanism for generating sound probabilistic over-approximations as a generalization of a well-known program abstraction technique known as predicate abstraction. Finally, the problem of inference and learning in the context of probabilistic program abstractions are briefly described.