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.