《Science of Computer Programming》：Slicing Assisted Program Verification: An Empirical Study
编辑推荐：
摘要形式化验证对于确保软件可靠性至关重要，但由于其高昂的资源消耗，在大规模系统中的应用仍然面临挑战。程序切片作为一种预处理技术被提出，旨在通过移除无关代码来节省验证开销；然而，其在多样化验证场景中的实际有效性尚未得到充分刻画。本文提出了一项全面的实证研究，通过多种技术工作流评
摘要
形式化验证对于确保软件可靠性至关重要，但由于其高昂的资源消耗，在大规模系统中的应用仍然面临挑战。程序切片作为一种预处理技术被提出，旨在通过移除无关代码来节省验证开销；然而，其在多样化验证场景中的实际有效性尚未得到充分刻画。本文提出了一项全面的实证研究，通过多种技术工作流评估程序切片与自动化验证的集成效果。我们针对可达性、终止性、有效解引用和无整数溢出四项属性，在广泛的C程序集合上进行了系统性考察，并深入探究了切片辅助验证的结果一致性、增强效果和程序适用性。
实验结果表明，程序切片引入的验证不一致性主要源于依赖分析不精确、验证器需求未满足以及结构修改。尽管切片在大多数实例中减少了验证时间，但在相当比例的子集中，由于过度切片开销或引入的语法复杂性，反而降低了效率。该方法对于具有松耦合、大量无关代码和简单数据流的程序更为有效，语义简化——而非单纯的代码缩减——才是推动性能提升的关键。我们的分析揭示，切片辅助验证的成功具有情境依赖性，受切片器能力、验证方法、程序特征和目标属性的影响。这些发现揭示了其优势与陷阱，在提供实用指导的同时，界定了当前的局限性和开放挑战。
引言
现代软件系统日益增长的复杂性给形式化验证带来了重大挑战。形式化验证旨在针对指定需求提供正确性的严格证明。作为一种根植于形式逻辑和离散数学的穷举分析技术，形式化验证在计算资源和人力投入方面往往代价高昂。因此，尽管具有重要的价值，自动化验证技术尚未被常规应用于大型、非平凡软件系统。
一种有前景的策略是将验证与简化目标系统的互补技术相结合，以提高验证的可扩展性和实用性。一个典型示例是将模型检测与程序切片相结合[1], [2], [3]。通常，这些方法首先将程序转换为抽象模型，然后根据特定属性应用切片来提取精简模型，最后在此较小模型上使用模型检测器。尽管这些切片增强方法在若干案例研究中展现了前景，但其在更广泛程序和属性范围内的普遍有效性和适用性仍需进一步系统调查。
当程序仅包含赋值、输出语句以及简单的控制流（如 if-then-else、while-do），且所有变量均为常量或标量而无指针时，基于程序依赖图/系统依赖图（PDG/SDG）的切片可以确保语义保持。即，如果程序在某输入上停止，则切片后的程序也会在该输入上停止并模拟原程序的行为[4], [5]。然而，这些保证对于具有指针、数组等复杂数据结构的真实C程序并不一定成立。我们调查切片器是否能够支持此类程序的精确分析，并评估在验证中应用切片所引入的潜在风险。为实证探索这一问题，本文报告了对切片增强验证方法的大规模评估，使用广泛应用的工具和知名的基准测试套件，包含大量C程序。
有几个关键问题值得深入探讨。首先，切片与验证之间存在根本性的目标差异：切片旨在移除所有与特定关注点无关的代码，而验证必须探索所有执行路径以保证违规的缺失。这引发了一个问题：切片是否会移除对健全验证过程至关重要的元素？其次，需要探索切片所实现的简化是否能转化为验证成本的显著节省，特别是在抽象解释[6]、有界模型检测[7]、CEGAR[8]和符号执行[9], [10]等多样且强大的现代验证技术下。第三个问题是何种类型的程序适合切片+验证的方法。例如，对于小型程序或切片本身开销超过验证投入的程序，收益可能微乎其微。据我们所知，现有研究缺乏对切片辅助验证有效性背后的原因和影响因素的全面分析与系统分类，而这些对于深入理解上述问题至关重要。为弥补这一空白，本文对实验结果进行了详细分析，并识别出影响切片–验证组合行为的重现因素。
在我们先前的论文[11]仅关注可达性属性的基础上，本工作大幅扩展了范围，对切片辅助验证呈现了全面的实证研究，并调查了该方法在多个关键验证属性上的有效性。与[11]相比的额外贡献包括：
- •
三个额外属性：终止性、有效解引用和无整数溢出，我们通过提出相应的切片准则将切片+验证技术扩展到这些属性。
- •
关于切片在验证中性能表现的关键实证发现，例如其属性依赖行为，通过定量评估和深入分析得出，以总结并刻画切片对验证的整体影响。
- •
对切片引入的陷阱进行详细分类，从识别导致验证结果不健全的根因以及切片过程引入的显著性能开销入手。
- •
有效切片-验证集成的成功条件，通过广泛的实验分析为组合方法提供可行的见解。
本文其余部分结构如下：第2节阐述基本概念和必要符号。第3节提出针对不同属性的切片准则和方法。第4节介绍研究问题和实验设置。第5节呈现实验结果及相关分析。第6节讨论相关工作。第7节阐述效度威胁，最后，第8节总结全文并提出未来工作。
章节摘要
面向属性的切片准则
程序验证优先考虑可达性、内存安全、并发安全、无整数溢出和终止性等关键属性的分析。然而，由于并发程序带来的独特挑战——特别是需要专门的切片技术来处理线程间通信和同步——本研究仅专注于顺序程序的属性。由于非法内存访问的普遍性和严重影响（包括
实验设计
我们首先概述实验评估旨在调查的研究问题，然后解释实验设置，最后详述我们的实现。
评估
为了系统解释观察到的验证不一致性和效率变化，我们通过实证分析推导出一组影响因素。具体而言，我们手动分析这些分类的根因，识别重现模式，并从源程序、切片和验证的角度进行分类。如表4所示，这些类别全面涵盖：PC 描述程序特征，CT 和 SC 捕获切片的效果和成本，
切片工具
针对Java程序有多种可用的切片工具，例如 Slicer4J [28]、JavaSlicer [29]、Indus [30] 和 JavaBST [31]。此外，近期研究探索了使用大语言模型对Java程序进行静态和动态切片，报告的准确率最高约为60%[32]。
虽然本研究专注于C程序的切片工具，但能够处理函数调用、指针和数组等高级C特性的静态切片工具数量有限
效度威胁
我们讨论了本研究可能面临的效度威胁，包括可能影响结果可靠性和可推广性的内部和外部因素。
结论与未来工作
我们通过广泛的实验，针对四项关键属性（可达性、终止性、有效解引用和无整数溢出），调查了将程序切片与验证集成以实现简化和成本节省的可行性与有效性。我们的详细比较和分析得出了以下关于切片辅助验证的优势与挑战的结论。
在积极方面，该方法展现了切片器的优势：Frama-C
CRediT作者贡献声明
Wenjian Chai：撰写–审阅与编辑，撰写–原稿，可视化，软件，方法论，调查，数据整理。Rongjie Yan：撰写–审阅与编辑，验证，指导，方法论，形式化分析。Wenhui Zhang：撰写–审阅与编辑，指导，方法论，概念化。Jian Zhang：撰写–审阅与编辑，项目管理，概念化。
利益冲突声明
作者声明不存在可能影响本文所报告工作的已知竞争性经济利益或个人关系。
Wenjian Chai|Rongjie Yan|Wenhui Zhang|Jian Zhang
