Skip to main content
PPGEE/UFAM

Artigo em periódicoOpen Access

ESBMC 6.1: automated test case generation using bounded model checking

GADELHA, M. Y. R.2020GADELHA, M. Y. R.; MENEZES, R.; CORDEIRO, L. C

2020 • International Journal on Software Tools for Technology Transfer • 25 citações

Resumo

Resumo

ESBMC is an SMT-based bounded model checker that provides a bit-precise verification of both C and C++ programs. Bounded model checking (BMC) was developed to provide faster results when finding property violations; BMC achieves this by limiting the number of loop unwindings and recursion depth. The technique, however, is unable to prove correctness unless all loops and recursions are fully unwound, which might not be possible for some programs (e.g., infinite loops). The version of ESBMC described here is designed to avoid the problem of guessing the number of unwindings, which leads to a property violation; it incrementally verifies the program, searching only for property violations. Once ESBMC has found a property violation, it produces a test suite that contains at least one test to expose a bug. ESBMC can correctly produce 312 test cases, which are confirmed by the test validator employed by Test-Comp 2019.

palavras-chave

Palavras-chave

ESBMCbounded model checkingautomated test generationSMT solversincremental verificationsoftware testing

Volume

23

Número

6

Páginas

857-861

Editora

Springer Science and Business Media LLC

Status

Published

links

DOI

10.1007/s10009-020-00571-2

Link Externo

https://doi.org/10.1007/s10009-020-00571-2

Repositório

https://research.manchester.ac.uk/en/publications/e04d4abe-22a4-48d8-9eb1-d5f0837f4a4d

Artigo em periódico

Electrocardiographic signal compression based on distributed source codingDE SOUZA, PATRESE E.B.2027DE SOUZA, PATRESE E.B.; DE LIMA FILHO, EDDIE B.; CORDEIRO, LUCAS C.; DE MELO, WHEIDIMA C.; DA SILVA, WALDIR S.; CARVALHO, CELSO B2027 • Biomedical Signal Processing and Control
Handling Asynchronous Scheduling Functions in Periodic Event-Triggered Gain-Scheduled Control With Guaranteed Polytopic InclusionCOUTINHO, Pedro Henrique Silva2026 COUTINHO, Pedro Henrique Silva; PESSIM, Paulo Sérgio Pereira; BESSA, Iury Valente; PEIXOTO, Márcia Luciana da Costa; PALHARES, Reinaldo Martinez2026 • IEEE Transactions on Cybernetics2citações
Systematic LMI approaches to design multivariable sliding mode controllers for uncertain systemsCOUTINHO, Pedro Henrique Silva2026COUTINHO, Pedro Henrique Silva; BESSA, Iury Valente; RODRIGUES, Victor Hugo Pereira; OLIVEIRA, Tiago Roux2026 • Automatica1citações
Finding software vulnerabilities in large C projects via bounded model checkingDE 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 C2026 • International Journal on Software Tools for Technology Transfer

Ver todas as publicações