Unsound validation for correctness witnesses by k-induction
The validation for correctness witnesses by k-induction might confirm wrong invariants and thus produces incorrect TRUE
results.
An example program equal-nested.c and a witness witness.graphml containing a wrong invariant.
A snippet of the program:
int main(void) {
unsigned int x = 0;
unsigned int y = 0;
while (__VERIFIER_nondet_int()) {
unsigned int z = 0;
while (__VERIFIER_nondet_int()) {
z++;
if (z == 2) x++;
}
x++;
y++;
}
__VERIFIER_assert(x==y);
return 0;
}
The program violates the specification, which can be confirmed by BMC:
./scripts/cpa.sh -spec sv-comp-reachability -bmc-incremental equal-nested.c
The witness contains a wrong invariant x==y
for the outer loop.
However, the witness validation based on k-induction wrongly confirms this invariant.
./scripts/cpa.sh -spec sv-comp-reachability -witnessValidation -witness witness.graphml -setprop witness.checkProgramHash=false equal-nested.c
The reason behind the unsoundness seems to be the following:
When k-induction checks the inductiveness of the invariant for the outer loop with k=1
, it only unrolls the inner loop once.
Therefore, it overlooks the counterexample to induction with z==2
, and the step case succeeds.
If the line if (z == 2) x++;
is replaced by if (z == 1) x++;
, the validation reports UNKNOWN
, which matches the above guess.