A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs
Programming Languages
2024-12-11 v1
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.
Cite
@article{arxiv.2412.07086,
title = {A Fixed Point Iteration Technique for Proving Correctness of Slicing for Probabilistic Programs},
author = {Torben Amtoft and Anindya Banerjee},
journal= {arXiv preprint arXiv:2412.07086},
year = {2024}
}
Comments
To be published by Springer in Festschrift for Alan Mycroft