Probabilistic horn clause verification

Abstract

Constrained Horn clauses have proven to be a natural intermediate language for logically characterizing program semantics and reasoning about program behavior. In this paper, we present probabilistically constrained Horn clauses (pchc), which incorporate probabilistic variables inside otherwise traditional constrained Horn clauses. pchc enable reasoning about probabilistic programs by encoding them as Horn clauses. Encoding probabilistic program semantics as pchc allows us to seamlessly handle procedure calls and recursion, as well as angelic and demonic forms of nondeterminism. We formalize pchc semantics and present a verification algorithm that can prove probabilistic safety properties of programs. We present an implementation and evaluation of our approach on a number of probabilistic programs and properties.