SMT-Based Bounded Model Checking for Multi-Threaded Software in Embedded Systems

The transition from single-core to multi-core processors has made multi-threaded software an important subject over the last years in computer-aided verification. Model checkers have been successfully applied to discover subtle errors, but they suffer from combinatorial state space explosion when verifying multi-threaded software. In the authors' previous work, they have extended the encodings from SMT-based Bounded Model Checking (BMC) to provide more accurate support for program verification and to use different background theories and solvers in order to improve scalability and precision in a completely automatic way.