Automated program verification ==> automation good.

But when fails, we don't know the solver state.

So we are doing "reverse tactic"

mechanically applying "reverse tactic" to identify the failing step.

high-level presentation about the problem and high-level contribution