View publication

Title Slicing of Probabilistic Programs based on Specifications
Authors Marcelo Navarro, Federico Olmedo
Publication date 2022
Abstract This paper presents the first slicing approach for
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.
Pages 102822
Volume 220
Journal name Science of Computer Programming
Publisher Elsevier Science (Amsterdam, The Netherlands)
Reference URL View reference page