ESBMC 6.1: automated test case generation using bounded model checking

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...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2021-12, Vol.23 (6), p.857-861
Main Authors: Gadelha, Mikhail R., Menezes, Rafael S., Cordeiro, Lucas C.
Format: Article
Language:English
Subjects:
Algorithms
Automation
C plus plus
Competitions and Challenges
Computer Science
Software
Software Engineering
Software Engineering/Programming and Operating Systems
Software testing
Theory of Computation
Violations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-020-00571-2