Program verification is concerned with proving that a program is
correct and adheres to a given specification. Testing a program, in
contrast, means to search for a witness that the program is
incorrect. In the present paper, we use a program logic for Java
to prove the incorrectness of programs. We show that this
approach, carried out in a sequent calculus for dynamic logic,
creates a connection between calculi and proof procedures for
program verification and test data generation procedures. In
comparison, starting with a program logic enables to find more
general and more complicated counterexamples for the correctness of
programs.