一句话：首次将全局公共子表达式消除（GCSE）引入形式验证，提出 VO-GCSE 并集成到 ESBMC 中以加速验证。
编译器优化的 GCSE 通过基于指向分析的可用表达式数据流去除冗余表达式，虽在 GCC、LLVM 中成功，但因符号内存模型与验证工具特性等挑战，在形式验证中尚未被探索。本文首次提出面向形式验证的 GCSE 算法 VO-GCSE，集成到 ESBMC 并复用其基于逻辑的基础设施（值集分析 VSA 与抽象解释 AI），将可用表达式数据流转化为抽象解释问题，并把 VSA 简化为指向分析。在 SV-COMP 基准、含 33 万个 C 样本的 FormAI 数据集及 Intel 真实验证用例上评估，结果表明 VO-GCSE 能减少具有相似解引用程序的验证时间，且抽象解释计算可用表达式不会使分析复杂化。
Compiler optimizations enhance the efficiency of machine code while maintaining its functionality. Global Common Subexpression Elimination (GCSE) removes redundant expressions using Available Expression (AE) data flow based on points-to-analysis. Despite its success in compilers such as GCC and LLVM, GCSE remains unexplored in Formal Verification (FV) due to domain-specific challenges. This paper is the first to introduce "Verification Optimization through GCSE" (VO-GCSE), a GCSE algorithm designed for FV, considering symbolic memory models and the unique attributes of FV tools. We integrated VO-GCSE into the Efficient SMT-based Context-Bounded Model Checker (ESBMC), leveraging its existing logic-based infrastructure, including Value-Set Analysis (VSA) and Abstract Interpretation (AI). We transformed AE data flow into an AI challenge and simplified VSA into points-to-analysis. VO-GCSE was evaluated using three diverse sources: the SV-COMP benchmarks, the FormAI dataset comprising 330, 000 C samples, and real-world verification cases from Intel. The experimental results show that (a) VO-GCSE reduces verification time for programs with similar dereferences, and (b) AE computation through AI does not complicate the analysis.
@inproceedings{paperbot9116,
title = {VO-GCSE: Verification Optimization through Global Common Subexpression Elimination},
author = {Rafael Sá Menezes and Norbert Tihanyi and Ridhi Jain and Alexander Levin and Rosiane de Freitas and Lucas C. Cordeiro},
booktitle = {FSE},
year = {2025},
doi = {10.1145/3696630.3728581}
}