We present an approach aiming at full functional deductive verification of
concurrent Java programs, based on symbolic execution. We define a Dynamic
Logic and a deductive verification calculus for a restricted fragment of Java
with native concurrency primitives. Even though we cannot yet deal with
non-atomic loops, employing the technique of symmetry reduction allows us to
verify unbounded systems.

The method relies on decision procedures for proving properties of data
structures and the applicability of symmetry reductions.

The calculus has been implemented within the KeY system, and we demonstrate it
by verifying a central method of the StringBuffer class from the Java standard
library.