Trabalho em anais de eventoOpen Access
VO-GCSE: Verification Optimization through Global Common Subexpression Elimination
MENEZES, RAFAEL SÁ; TIHANYI, NORBERT; JAIN, RIDHI; LEVIN, ALEXANDER; DE FREITAS, ROSIANE; CORDEIRO, LUCAS C
Resumo
Resumo
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.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
formal verificationcompiler optimizationpoints-to analysisabstract interpretationESBMCSMT solvers
Status
Published
links
Links e arquivos
Trabalho em anais de evento