A theory of slicing for probabilistic control flow graphs

DOI10.1007/978-3-662-49630-5_11MaRDI QIDQ2811339zbMATHOpenAlexFDO

Authors Torben Amtoft, Anindya Banerjee

Publication date 10 June 2016

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1711.02246

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We present a theory for slicing probabilistic imperative programs -- containing random assignments, and ``observe statements (for conditioning) -- represented as probabilistic control-flow graphs (pCFGs) whose nodes modify probability distributions. We show that such a representation allows direct adaptation of standard machinery such as data and control dependence, postdominators, relevant variables, etc to the probabilistic setting. 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. To generate smaller slices, we may in addition take advantage of knowledge that certain loops will terminate (almost) always. A key feature of our syntactic conditions is that they involve two disjoint slices such that the variables of one slice are probabilistically independent of the variables of the other. This leads directly to a proof of correctness of probabilistic slicing. In a companion article we show adequacy of the semantics of pCFGs with respect to the standard semantics of structured probabilistic programs.

Recommendations

• Program Slicing
• Assertion-based slicing and slice graphs
• On slicing of programs with input statements
• On probabilistic techniques for data flow analysis
• Understanding probabilistic programs

Cites work

• A theory of slicing for probabilistic control flow graphs
• A unifying theory of control dependence and its application to arbitrary program structures
• Labelled Markov processes.
• Program Slicing
• Semantics of probabilistic programs
• Slicing for modern program structures: a theory for eliminating irrelevant loops

Cited in

(2)

• A theory of slicing for probabilistic control flow graphs
• Efficient computation of arbitrary control dependencies

This page was built for publication: A theory of slicing for probabilistic control flow graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811339)