一句话:提出 2clever,通过在控制流中搜索影响边界,高效求解客户端特定等价性检查问题。
客户端特定等价性检查(CSEC)旨在从保持不变的客户端视角分析下游组件(库)变更带来的影响。已有的通用技术(如回归验证、等价性检查)或专用技术应用于 CSEC 时,要么要求用户提供规约,要么难以扩展到实际规模。本文提出一种新的 CSEC 求解方案 2clever,其核心思想是在程序控制流中搜索“影响边界”,从而将库变更影响的分析限制在相关范围之内。作者实现了一个原型系统,并在一个覆盖广泛的基准测试集上进行了评估,结果表明该原型与当前最先进的技术相比具有良好性能。
Client-specific equivalence checking (CSEC) is a technique proposed previously to perform impact analysis of changes to downstream components (libraries) from the perspective of an unchanged system (client). Existing analysis techniques, whether general (regression verification, equivalence checking) or special-purpose, when applied to CSEC, either require users to provide specifications, or do not scale. We propose a novel solution to the CSEC problem, called 2clever, that is based on searching the control-flow of a program for impact boundaries. We evaluate a prototype implementation of 2clever on a comprehensive set of benchmarks and conclude that our prototype performs well compared to the state-of-the-art.