Page 1,2: Running example in the Introduction:
The invariant is
(pc = inc => x = 0) AND (pc = dec => (x = 0 OR x = 2))
and not
(pc = inc => x = 0) AND (pc = dec => x = 2).
Page 8: Lemma 4 and subsequent remarks:
Lemma 4 assumes that the $R$-Simplify function is equiv-
alence preserving. Later, in Section 4.3, we say that
R-Simplify can weaken a formula. The correctness with
the weakening is outlined later.
However, Lemma 5, Lemma 6 and Theorem 2 hold true in
the case when R-Simplify weakens a formula.
Page 9: Lemma 6:
$\psi$ is not contained in Reach, but only has a nonempty
intersection with $Reach$.
Page 9: Just before description of the InvGen procedure:
It says that $\psi$ is an under-approximation and $phi$
an over-approximation of the reachable state set. If we
use R-Simplify in propagation, as described in the paper
and assume it is not equivalence preserving, then this is
no longer true. But, this doesnot effect the correctness
(Theorem 2) of the procedure.
Theorem 3, Page 11:
In a downward iteration sequence with narrowing, we can
apply simplification rule (i.e. R-Simplify) only after a
propagation step and not after a narrowing step. (The
statement of Theorem 3 is more general and suggests that
we can R-Simplify any formula in a downward iteration
sequence, which is not true.)