a dynamic constraint-based bmc strategy for generating counterexamples
Checking safety properties is mandatory in the validation process of critical software. When formal verification tools fail to prove some properties, the automatic generation of counterexamples for a given loop depth is achievable, and is therefore an important issue in practice. We propose in this paper a dynamic constraint based exploration strategy for software bounded model checking. Constraint solving is integrated with state exploration to prune state space. Experiments on a real industrial Flasher Manager controller show that our system outperforms state of the art bounded model checking tools.
counterexamples bounded model checking constraint programming program testing dynamic exploration strategy