  The complexity of software in embedded systems has increased significantly
over the last years so that software verification now plays an important role
in ensuring the overall product quality. In this context, SAT-based bounded
model checking has been successfully applied to discover subtle errors, but for
larger applications, it often suffers from the state space explosion problem.
This paper describes a new approach called continuous verification to detect
design errors as quickly as possible by looking at the Software Configuration
Management (SCM) system and by combining dynamic and static verification to
reduce the state space to be explored. We also give a set of encodings that
provide accurate support for program verification and use different background
theories in order to improve scalability and precision in a completely
automatic way. A case study from the telecommunications domain shows that the
proposed approach improves the error-detection capability and reduces the
overall verification time by up to 50%.
