This paper presents a quantitative program verification infrastructure for discrete
probabilistic programs.
Our infrastructure can be viewed as the probabilistic analogue of Boogie:
its central components are an intermediate verification language (IVL) together with a real-valued logic.
Our IVL provides a programming-language-style for expressing verification
conditions whose validity implies the correctness of a program under investigation.
As our
focus is on verifying quantitative properties such as bounds on
expected outcomes, expected run-times, or termination
probabilities, off-the-shelf IVLs based on Boolean first-order logic do not
suffice.
Instead, a paradigm shift from the standard Boolean to a real-valued domain is required.

Our IVL features quantitative generalizations of standard
verification constructs such as assume- and assert-statements. Verification conditions are generated by a
weakest-precondition-style semantics, based on our real-valued logic.
We show that
our verification infrastructure supports natural encodings of numerous verification
techniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification
infrastructure for expectation-based reasoning about probabilistic programs.