Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)

TL;DR

This paper introduces slicing techniques for probabilistic program verification to improve error localization, proof simplification, and verification success preservation, with a formal foundation and practical implementation in the Caesar verifier.

Contribution

It formalizes slicing notions for probabilistic programs, introduces a new error localization method, and implements these diagnostics in the Caesar verifier with empirical evaluation.

Findings

Slicing-based diagnostics effectively localize errors in probabilistic programs.

Brutus can find small, informative slices that aid in debugging and verification.

Empirical results show improved error detection and proof simplification.

Abstract

This paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. Our key principle is based on providing slices for (1) error reporting, (2) proof simplification, and (3) preserving successful verification results. By formally defining these different 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 is a novel notion of error localization for quantitative assertions. 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. We implemented our user diagnostics into the deductive verifier Caesar. Our novel implementation -- called \emph{Brutus} -- can search for slices which do or do not verify, corresponding to each of the three diagnostic notions. For error reporting (1), it exploits a binary search-based algorithm that minimizes error-witnessing slices. To solve for slices that verify (2 and 3), we empirically compare different algorithms based on unsatisfiable cores, minimal unsatisfiable subset enumeration, and a direct SMT encoding of the slicing problem. Our empirical evaluation of Brutus on existing and new benchmarks shows that we can find slices that are both small and informative.