Program Verification as Probabilistic Inference
Abstract
In this paper, we propose a new algorithm for proving the validity
or invalidity of a pre/postcondition pair for a program. The
algorithm is motivated by the success of the algorithms for
probabilistic inference developed in the machine learning
community for reasoning in graphical models. The validity or
invalidity proof consists of providing an invariant at each
program point that can be locally verified. The algorithm works by
iteratively randomly selecting a program point and updating the
current abstract state representation to make it more locally
consistent (with respect to the abstractions at the neighboring
points). We show that this simple algorithm has some interesting
aspects: (a) It brings together the complementary powers of
forward and backward analyses; (b) The algorithm has the ability
to recover itself from excessive under-approximation or
over-approximation that it may make. (Because the algorithm does
not distinguish between the forward and backward information, the
information could get both under-approximated and
over-approximated at any step.) (c) The randomness in the
algorithm ensures that the correct choice of updates is
eventually made as there is no single deterministic strategy that
would provably work for any interesting class of programs. In our
experiments we use this algorithm to produce the proof of
correctness of a small (but non-trivial) example.
In addition, we empirically illustrate several important
properties of the algorithm.