A Theory of Slicing for Probabilistic Control Flow Graphs

The task of program slicing is to remove the parts of a program that are irrelevant in a given context. In probabilistic programs, where variables may be assigned random values from a given distribution, and undesirable combinations of values may be removed by “observe” statements, the standard notions of data and control dependence no longer suffice for semantically correct slicing, as demonstrated by Hur et al. in recent work. This paper presents a theory for slicing probabilistic programs, represented as control flow graphs whose nodes transform probability distributions. We separate the specification of slicing from its implementation: first we develop syntactic conditions that a slice must satisfy; next we prove that any such slice is semantically correct; finally we give an algorithm to compute the least slice. We state correctness in terms of observational equivalence between the behaviors of the sliced program and of the original. A program’s behavior is its final p...

• Type: Journal
• Year: 2016
• Where: FOSSACS
• Authors: Torben Amtoft, Anindya Banerjee
• Keywords: FOSSACS 2016, Software Engineering