Continuous verification of large embedded software using SMT-based bounded model checking

The complexity of software in embedded systems has in-creased significantly over the last years so that software ver-ification now plays an important role in ensuring the over-all product quality. In this context, bounded model check-ing 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 ap-proach called continuous verification to detect design er-rors as quickly as possible by exploiting information from the software configuration management system and by com-bining 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 scalabil-ity 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%.