ESBMC 6.1: automated test case generation using bounded model checking

Mikhail R Gadelha, Rafael Menezes, Lucas Cordeiro

Research output: Contribution to journalArticlepeer-review

6 Downloads (Pure)


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.
Original languageEnglish
Pages (from-to)857–861
JournalInternational Journal on Software Tools for Technology Transfer
Publication statusPublished - 18 May 2020


Dive into the research topics of 'ESBMC 6.1: automated test case generation using bounded model checking'. Together they form a unique fingerprint.

Cite this