一句话：为过程间且可能非终止程序上的一类基于依赖的切片方法给出通用语义正确性证明。
现有基于依赖的切片正确性证明要么只覆盖过程内程序，要么只适用于特定切片方法。本文针对过程间且可能非终止的程序，给出一类基于依赖切片方法的通用正确性证明，涵盖 Weiser 与 Binkley 等人的方法。证明基于良构的弱/强控制闭包关系，这是 Danicic 等人一般化弱/强控制闭包的过程间扩展，可刻画文献中多种非终止不敏感与非终止敏感的控制依赖关系。文中定义语义正确切片，并证明其与 Weiser 切片一致；确定性 SC 切片保持终止性，非确定性 SC 切片保持原程序的非确定性行为。
Existing proofs of correctness for dependence-based slicing methods are limited either to the slicing of intraprocedural programs [2, 39], or the proof is only applicable to a specific slicing method [4, 41]. We contribute a general proof of correctness for dependence-based slicing methods such as Weiser [50, 51], or Binkley et al. [7, 8], for interprocedural, possibly nonterminating programs. The proof uses well-formed weak and strong control closure relations, which are the interprocedural extensions of the generalised weak/strong control closure provided by Danicic et al. [13], capturing various nonterminating-insensitive and nontermination-sensitive control-dependence relations that have been proposed in the literature. Thus, our proof framework is valid for a whole range of existing control-dependence relations. We have provided a definition of semantically correct (SC) slice. We prove that SC slices agree with Weiser slicing, that deterministic SC slices preserve termination, and that nondeterministic SC slices preserve the nondeterministic behavior of the original programs.
@article{MasudL21,
title = {Semantic Correctness of Dependence-based Slicing for Interprocedural, Possibly Nonterminating Programs},
author = {Abu Naser Masud and Björn Lisper},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {42},
number = {4},
year = {2020},
doi = {10.1145/3434489}
}