This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing different kinds of slices for (1) error reporting, (2) proof simplification, and (3) preserving succesful verification results. By formally defining these notions on HeyVL, an existing quantitative intermediate verification language (IVL), our concepts (and implementation) can be used to obtain diagnostics for a range of probabilistic programming languages. Slicing for error reporting provides the first formal definition of error localization for quantitative assertion statements. We demonstrate slicing-based diagnostics on a variety of proof rules such as quantitative versions of the specification statement and invariant-based loop rules, and formally prove the correctness of specialized error messages and verification hints.

As our approach is based on a conservative extension of Boolean IVLs, our results apply to non-probabilistic deductive verification such as Dafny or Viper.

We implemented our user diagnostics into the deductive verifier Caesar. Our implementation — dubbed Brutus — can search for verifying or error slices. We empirically evaluate Brutus on a set of benchmarks from the literature, as well as on new benchmarks. To solve for slices that verify, we empirically compare different algorithms based on unsatisfiable cores, minimal unsatisfiable subset enumeration, and a direct encoding of the slicing problem to SMT. These searches are integrated into Caesar to generate user diagnostics.