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

Philipp Schröer, Darion Haase, Joost-Pieter Katoen

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…