Skip to main content

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

2025 • 28th International Conference on Fundamental Approaches to Software Engineering • 3 citações

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

Trabalho em anais de evento