We present MODL, a Dynamic Logic and a deductive verification calculus
for a core Java-like language that includes multi-threading. The
calculus is based on symbolic execution. Even though we currently do not
handle non-atomic loops, employing the technique of symmetry reduction
allows us to verify systems without limits on state space or thread
number. We have instantiated our logic for (restricted) multi-threaded
Java programs and implemented the verification calculus within the KeY
system. We demonstrate our approach by verifying a central method of the
StringBuffer class from the Java standard library in the presence of
unbounded concurrency.