Trabalho em anais de eventoOpen Access
ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving (Competition Contribution)
WEI, C.; WU, T.; MENEZES, R.; SHMAROV, F.; ALJAAFARI, FATIMAH K.; GODBOLEY, S.; ALSHMRANY, K.; RODRIGUES, R. F.; CORDEIRO, L. C
Resumo
Resumo
Abstract ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the category of Test-Comp 2025.
palavras-chave
Palavras-chave
ESBMCSMT solversbounded model checkingtest suite generationsoftware verification
Status
Published
links
Links e arquivos
Trabalho em anais de evento