Slicing of Probabilistic Programs based on Specifications

TL;DR

This paper introduces a novel slicing method for probabilistic programs that leverages specifications to produce more precise, correctness-preserving slices using backward propagation of post-conditions and formal verification techniques.

Contribution

It presents the first specification-based slicing approach for probabilistic programs, utilizing the greatest pre-expectation transformer and formal correctness proofs.

Findings

More precise slices than conventional dependency-based methods

Formal verification condition generators for probabilistic correctness

Practical applicability demonstrated through examples and a case study

Abstract

This paper presents the first slicing approach for probabilistic programs based on specifications. We show that when probabilistic programs are accompanied by their specifications in the form of pre- and post-condition, we can exploit this semantic information to produce specification-preserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency. To achieve this goal, our technique is based on the backward propagation of post-conditions via the greatest pre-expectation transformer -- the probabilistic counterpart of Dijkstra weakest pre-condition transformer. The technique is termination-sensitive, allowing to preserve the partial as well as the total correctness of probabilistic programs w.r.t. their specifications. It is modular, featuring a local reasoning principle, and is formally proved correct. As fundamental technical ingredients of our technique, we design and prove sound verification condition generators for establishing the partial and total correctness of probabilistic programs, which are of interest on their own and can be exploited elsewhere for other purposes. On the practical side, we demonstrate the applicability of our approach by means of a few illustrative examples and a case study from the probabilistic modelling field. We also describe an algorithm for computing least slices among the space of slices derived by our technique.