Improving Saturation-based Bounded Model Checking

Formal verification is becoming a fundamental step in assuring thecorrectness of safety-critical systems. Since these systems are oftenasynchronous and even distributed, their verification requires methodsthat can deal with huge or even infinite state spaces. Model checkingis one of the current techniques to analyse the behaviour of systems,as part of the verification process. In this paper a symbolic boundedmodel checking algorithm is presented that relies on efficient saturation-basedmethods. The previous approaches are extended with new bounded statespace exploration strategies. In addition, constrained saturationis also introduced to improve the efficiency of bounded model checking.Our measurements confirm that these approaches do not only offera solution to deal with infinite state spaces, but in many casesthey even outperform the original methods.