Slicing for modern program structures: a theory for eliminating irrelevant loops

Slicing is a program transformation technique with numerous applications, as it allows the user to focus on the parts of a program that are relevant for a given purpose. Ideally, the slice program should have the same termination properties as the original program, but to keep the slices manageable, it might be preferable to slice away loops that do not affect the values of relevant variables. This paper provides the first theoretical foundation to reason about non-termination insensitive slicing without assuming the presence of a unique end node. A slice is required to be closed under data dependence and under a recently proposed variant of control dependence, called weak order dependence. This allows a simulation-based correctness proof for a correctness criterion stating that the observational behavior of the original program must be a prefix of the behavior of the slice program.