VO-GCSE: Verification Optimization through Global Common Subexpression Elimination

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.