  Identifying the cause of a proof failure during deductive verification of
programs is hard: it may be due to an incorrectness in the program, an
incompleteness in the program annotations, or an incompleteness of the prover.
The changes needed to resolve a proof failure depend on its category, but the
prover cannot provide any help on the categorisation. When using an SMT solver
to discharge a proof obligation, that solver can propose a model from a failed
attempt, from which a possible counterexample can be derived. But the
counterexample may be invalid, in which case it may add more confusion than
help. To check the validity of a counterexample and to categorise the proof
failure, we propose the comparison between the run-time assertion-checking
(RAC) executions under two different semantics, using the counterexample as an
oracle. The first RAC execution follows the normal program semantics, and a
violation of a program annotation indicates an incorrectness in the program.
The second RAC execution follows a novel "giant-step" semantics that does not
execute loops nor function calls but instead retrieves return values and values
of modified variables from the oracle. A violation of the program annotations
only observed under giant-step execution characterises an incompleteness of the
program annotations. We implemented this approach in the Why3 platform for
deductive program verification and evaluated it using examples from prior
literature.
