A dynamic constraint-based BMC strategy for generating counterexamples
Hélène Collavizza, Nguyen Le Vinh, Michel Rueher, Samuel Devulder, Thierry Gueguen · 2011
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.