Safety Verification and Refutation by $k$-Invariants and $k$-Induction