Verification and falsification of programs with loops using predicate abstraction