A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs

TL;DR

This paper introduces a fixed point iteration method with a non-standard starting point to prove the correctness of slicing in probabilistic programs, providing a general framework and application insights.

Contribution

It presents a novel fixed point iteration technique with a specific starting point for verifying program slicing correctness in probabilistic programs.

Findings

Established lemmas for applying the technique

Outlined application to probabilistic program slicing

Demonstrated the method's effectiveness

Abstract

When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.