Artigo em periódicoOpen Access
Finding software vulnerabilities in large C projects via bounded model checking
DE SOUSA, JANISLLEY O.2026DE SOUSA, JANISLLEY O.; DE FARIAS, BRUNO C.; DA SILVA, THALES A.; TIHANYI, NORBERT; DUBNICZKY, RICHARD A.; FILHO, EDDIE B. L.; CORDEIRO, LUCAS C
Resumo
Resumo
Abstract Bounded model checking (BMC) is a widely used technique for detecting security vulnerabilities and verifying the correctness of critical software components. While highly effective on small to medium-sized codebases, its application to large-scale software systems remains difficult due to scalability limitations. In this work, we present a practical methodology to enable the use of BMC in real-world, complex software projects. Our approach includes automated preprocessing of source code and a guided verification process that helps a model checker systematically explore a codebase. We also introduce a function-level prioritization mechanism that focuses verification efforts on the most critical code parts. We evaluated our method on popular open-source C projects, discovering security vulnerabilities that the respective developers confirmed. The results demonstrate that, with appropriate strategies, BMC can effectively scale to verify large software systems while maintaining low memory usage.
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
bounded model checkingsoftware vulnerabilitiesvulnerability detectionscalabilitysource code preprocessingC programsopen source softwarememory usage
Volume
1
Páginas
1
Editora
Springer Science and Business Media LLC
Status
Published
links
Links e arquivos
Artigo em periódico