  Computer-based systems have been used to solve several domain problems, such
as industrial, military, education, and wearable. Those systems need
high-quality software to guarantee security and safety. We advocate that
Bounded Model Checking (BMC) techniques can detect security vulnerabilities in
the early stages of development processes. However, this technique struggles to
scale up and verify large software commonly found on computer-based systems.
Here, we develop and evaluate a pragmatic approach to verify large software
systems using a state-of-the-art bounded model checker. In particular, we
pre-process the input source-code files and then guide the model checker to
explore the code systematically. We also present a multi-core implementation of
the k-induction proof algorithm to verify and falsify large software systems
iteratively. Our experimental results using the Efficient SMT-based Model
Checker (ESBMC) show that our approach can guide ESBMC to efficiently verify
large software systems. We evaluate our approach using the PuTTY application to
verify 136 files and 2803 functions in less than 86 minutes, and the SlimGuard
allocator, where we have found real security vulnerabilities confirmed by the
developers. We conclude that our approach can successfully guide a bounded
model checker to verify large software systems systematically.
